Mathlib.LinearAlgebra.LinearIndependent.Defs

LinearIndependent definition

: Prop

Full source

/-- `LinearIndependent R v` states the family of vectors `v` is linearly independent over `R`. -/
def LinearIndependent : Prop :=
  Injective (Finsupp.linearCombination R v)

Linear independence of a family of vectors

Informal description

A family of vectors $ v : \iota \to M $ is called linearly independent over $ R $ if the linear combination map $ \text{Finsupp.linearCombination}_R v : (\iota \to_{\text{f}} R) \to M $ is injective. Here $ (\iota \to_{\text{f}} R) $ denotes the space of finitely supported functions from $ \iota $ to $ R $, and the linear combination map sends a finitely supported function $ f $ to the sum $ \sum_{i \in \text{supp}(f)} f(i) \cdot v(i) $.

delabLinearIndependent definition

: Delab

Full source

/-- Delaborator for `LinearIndependent` that suggests pretty printing with type hints
in case the family of vectors is over a `Set`.

Type hints look like `LinearIndependent fun (v : ↑s) => ↑v` or `LinearIndependent (ι := ↑s) f`,
depending on whether the family is a lambda expression or not. -/
@[app_delab LinearIndependent]
def delabLinearIndependent : Delab :=
  whenPPOption getPPNotation <|
  whenNotPPOption getPPAnalysisSkip <|
  withOptionAtCurrPos `pp.analysis.skip true do
    let e ← getExpr
    guardguard <| e.isAppOfArity ``LinearIndependent 7
    let somesome _ := (e.getArg! 0).coeTypeSet? | failure
    let optionsPerPos ← if (e.getArg! 3).isLambda then
      withNaryArg 3 do return (← read).optionsPerPos.setBool (← getPos) pp.funBinderTypes.name true
    else
      withNaryArg 0 do return (← read).optionsPerPos.setBool (← getPos) `pp.analysis.namedArg true
    withTheReader Context ({· with optionsPerPos}) delab

Delaborator for Linear Independence with Type Hints

Informal description

The delaborator for `LinearIndependent` provides pretty printing with type hints when the family of vectors is defined over a set. It suggests notations like `LinearIndependent fun (v : ↑s) => ↑v` or `LinearIndependent (ι := ↑s) f` depending on whether the family is a lambda expression or not.

LinearIndepOn definition

(s : Set ι) : Prop

Full source

/-- `LinearIndepOn R v s` states that the vectors in the family `v` that are indexed
by the elements of `s` are linearly independent over `R`. -/
def LinearIndepOn (s : Set ι) : Prop := LinearIndependent R (fun x : s ↦ v x)

Linear independence on a subset of indices

Informal description

Given a family of vectors $v : \iota \to M$ over a ring $R$ and a subset $s \subseteq \iota$, the vectors $\{v_i\}_{i \in s}$ are called *linearly independent over $R$* if the restricted family $(v \restriction s) : s \to M$ is linearly independent. This means that the only finite linear combination $\sum_{i \in s} c_i v_i = 0$ with coefficients $c_i \in R$ is the trivial one where all $c_i = 0$.

LinearIndepOn.linearIndependent theorem

{s : Set ι} (h : LinearIndepOn R v s) : LinearIndependent R (fun x : s ↦ v x)

Full source

theorem LinearIndepOn.linearIndependent {s : Set ι} (h : LinearIndepOn R v s) :
    LinearIndependent R (fun x : s ↦ v x) := h

Linear independence of a restricted family from linear independence on a subset

Informal description

For any subset $s \subseteq \iota$, if the family of vectors $\{v_i\}_{i \in s}$ is linearly independent over $R$, then the restricted family $(v \restriction s) : s \to M$ is linearly independent over $R$.

linearIndependent_iff_injective_finsuppLinearCombination theorem

: LinearIndependent R v ↔ Injective (Finsupp.linearCombination R v)

Full source

theorem linearIndependent_iff_injective_finsuppLinearCombination :
    LinearIndependentLinearIndependent R v ↔ Injective (Finsupp.linearCombination R v) := Iff.rfl

Characterization of Linear Independence via Injectivity of Linear Combination Map

Informal description

A family of vectors $v : \iota \to M$ is linearly independent over a ring $R$ if and only if the linear combination map $\text{Finsupp.linearCombination}_R v : (\iota \to_{\text{f}} R) \to M$ is injective. Here, $(\iota \to_{\text{f}} R)$ denotes the space of finitely supported functions from $\iota$ to $R$, and the linear combination map sends a finitely supported function $f$ to the sum $\sum_{i \in \text{supp}(f)} f(i) \cdot v(i)$.

linearIndependent_iff_injective_fintypeLinearCombination theorem

[Fintype ι] : LinearIndependent R v ↔ Injective (Fintype.linearCombination R v)

Full source

theorem linearIndependent_iff_injective_fintypeLinearCombination [Fintype ι] :
    LinearIndependentLinearIndependent R v ↔ Injective (Fintype.linearCombination R v) := by
  simp [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearIndependent]

Linear independence via injectivity of finite linear combinations

Informal description

For a finite type $\iota$, a family of vectors $v : \iota \to M$ is linearly independent over a ring $R$ if and only if the linear combination map $(\sum_{i \in \iota} f(i) \cdot v(i))$ is injective on functions $f : \iota \to R$.

LinearIndependent.injective theorem

[Nontrivial R] (hv : LinearIndependent R v) : Injective v

Full source

theorem LinearIndependent.injective [Nontrivial R] (hv : LinearIndependent R v) : Injective v := by
  simpa [comp_def]
    using Injective.comp hv (Finsupp.single_left_injective one_ne_zero)

Linear independence implies injectivity of the vector family

Informal description

Let $R$ be a nontrivial ring and $M$ be an $R$-module. A family of vectors $v : \iota \to M$ is linearly independent over $R$ if and only if the map $v$ is injective.

LinearIndepOn.injOn theorem

[Nontrivial R] (hv : LinearIndepOn R v s) : InjOn v s

Full source

theorem LinearIndepOn.injOn [Nontrivial R] (hv : LinearIndepOn R v s) : InjOn v s :=
  injOn_iff_injective.2 <| LinearIndependent.injective hv

Injectivity of Linearly Independent Vectors on a Subset

Informal description

Let $R$ be a nontrivial ring and $M$ an $R$-module. Given a family of vectors $v : \iota \to M$ and a subset $s \subseteq \iota$, if the vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$, then the restriction of $v$ to $s$ is injective. In other words, for any $i, j \in s$, if $v_i = v_j$, then $i = j$.

LinearIndependent.smul_left_injective theorem

(hv : LinearIndependent R v) (i : ι) : Injective fun r : R ↦ r • v i

Full source

theorem LinearIndependent.smul_left_injective (hv : LinearIndependent R v) (i : ι) :
    Injective fun r : R ↦ r • v i := by convert hv.comp (Finsupp.single_injective i); simp

Injectivity of Scalar Multiplication on Linearly Independent Vectors

Informal description

Let $R$ be a ring and $M$ an $R$-module. For a linearly independent family of vectors $v : \iota \to M$ and any index $i \in \iota$, the scalar multiplication map $r \mapsto r \cdot v_i$ is injective. In other words, if $r_1 \cdot v_i = r_2 \cdot v_i$ for some $r_1, r_2 \in R$, then $r_1 = r_2$.

LinearIndependent.ne_zero theorem

[Nontrivial R] (i : ι) (hv : LinearIndependent R v) : v i ≠ 0

Full source

theorem LinearIndependent.ne_zero [Nontrivial R] (i : ι) (hv : LinearIndependent R v) :
    v i ≠ 0 := by
  intro h
  have := @hv (Finsupp.single i 1 : ι →₀ R) 0 (by simpa using h)
  simp at this

Nonzero Vectors in a Linearly Independent Family

Informal description

For any nontrivial ring $R$ and any linearly independent family of vectors $v : \iota \to M$ over $R$, each vector $v_i$ in the family is nonzero. That is, if $v$ is linearly independent, then $v_i \neq 0$ for every index $i \in \iota$.

LinearIndepOn.ne_zero theorem

[Nontrivial R] {i : ι} (hv : LinearIndepOn R v s) (hi : i ∈ s) : v i ≠ 0

Full source

theorem LinearIndepOn.ne_zero [Nontrivial R] {i : ι} (hv : LinearIndepOn R v s) (hi : i ∈ s) :
    v i ≠ 0 :=
  LinearIndependent.ne_zero ⟨i, hi⟩ hv

Nonzero Vectors in a Linearly Independent Subfamily

Informal description

Let $R$ be a nontrivial ring and $M$ an $R$-module. Given a subset $s \subseteq \iota$ and a family of vectors $v : \iota \to M$ that is linearly independent on $s$, then for any index $i \in s$, the vector $v_i$ is nonzero, i.e., $v_i \neq 0$.

LinearIndepOn.zero_not_mem_image theorem

[Nontrivial R] (hs : LinearIndepOn R v s) : 0 ∉ v '' s

Full source

theorem LinearIndepOn.zero_not_mem_image [Nontrivial R] (hs : LinearIndepOn R v s) : 0 ∉ v '' s :=
  fun ⟨_, hi, h0⟩ ↦ hs.ne_zero hi h0

Zero Vector Not in Image of Linearly Independent Subfamily

Informal description

For a nontrivial ring $R$ and a family of vectors $v : \iota \to M$ over $R$, if the vectors $\{v_i\}_{i \in s}$ are linearly independent on a subset $s \subseteq \iota$, then the zero vector $0$ is not in the image of $s$ under $v$, i.e., $0 \notin v(s)$.

linearIndependent_empty_type theorem

[IsEmpty ι] : LinearIndependent R v

Full source

theorem linearIndependent_empty_type [IsEmpty ι] : LinearIndependent R v :=
  injective_of_subsingleton _

Linear Independence of Vectors Indexed by Empty Type

Informal description

For any empty indexing type $\iota$ and any family of vectors $v : \iota \to M$ over a ring $R$, the family $v$ is linearly independent.

linearIndependent_zero_iff theorem

[Nontrivial R] : LinearIndependent R (0 : ι → M) ↔ IsEmpty ι

Full source

@[simp]
theorem linearIndependent_zero_iff [Nontrivial R] : LinearIndependentLinearIndependent R (0 : ι → M) ↔ IsEmpty ι :=
  ⟨fun h ↦ not_nonempty_iff.1 fun ⟨i⟩ ↦ (h.ne_zero i rfl).elim,
    fun _ ↦ linearIndependent_empty_type⟩

Linear Independence of Zero Family Equivales Empty Index Type

Informal description

For a nontrivial ring $R$ and a module $M$ over $R$, the zero family of vectors $0 : \iota \to M$ is linearly independent if and only if the indexing type $\iota$ is empty.

linearIndepOn_zero_iff theorem

[Nontrivial R] : LinearIndepOn R (0 : ι → M) s ↔ s = ∅

Full source

@[simp]
theorem linearIndepOn_zero_iff [Nontrivial R] : LinearIndepOnLinearIndepOn R (0 : ι → M) s ↔ s = ∅ :=
  linearIndependent_zero_iff.trans isEmpty_coe_sort

Linear Independence of Zero Family on Subset Equivales Empty Subset

Informal description

For a nontrivial ring $R$ and a module $M$ over $R$, the zero family of vectors $0 : \iota \to M$ is linearly independent on a subset $s \subseteq \iota$ if and only if $s$ is the empty set.

linearIndependent_empty theorem

: LinearIndependent R (fun x => x : (∅ : Set M) → M)

Full source

theorem linearIndependent_empty : LinearIndependent R (fun x => x : (∅ : Set M) → M) :=
  linearIndependent_empty_type

Linear Independence of the Empty Family of Vectors

Informal description

The family of vectors indexed by the empty set $\emptyset$ in a module $M$ over a ring $R$ is linearly independent. That is, the map $(x \mapsto x) : \emptyset \to M$ is linearly independent.

linearIndepOn_empty theorem

: LinearIndepOn R v ∅

Full source

@[simp]
theorem linearIndepOn_empty : LinearIndepOn R v ∅ :=
  linearIndependent_empty_type ..

Linear Independence of Vectors Indexed by Empty Set

Informal description

For any family of vectors $v : \iota \to M$ over a ring $R$, the vectors indexed by the empty set $\emptyset \subseteq \iota$ are linearly independent.

linearIndependent_set_coe_iff theorem

: LinearIndependent R (fun x : s ↦ v x) ↔ LinearIndepOn R v s

Full source

theorem linearIndependent_set_coe_iff :
    LinearIndependentLinearIndependent R (fun x : s ↦ v x) ↔ LinearIndepOn R v s := Iff.rfl

Equivalence of Linear Independence for Restricted Family and Subset

Informal description

For a family of vectors $v : \iota \to M$ over a ring $R$ and a subset $s \subseteq \iota$, the restricted family $(v \restriction s) : s \to M$ is linearly independent over $R$ if and only if the vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$.

linearIndependent_subtype_iff theorem

{s : Set M} : LinearIndependent R (Subtype.val : s → M) ↔ LinearIndepOn R id s

Full source

theorem linearIndependent_subtype_iff {s : Set M} :
    LinearIndependentLinearIndependent R (Subtype.val : s → M) ↔ LinearIndepOn R id s := Iff.rfl

Equivalence of Linear Independence for Subset Inclusion and Identity Function

Informal description

For any subset $s$ of an $R$-module $M$, the family of vectors obtained by including $s$ into $M$ (via the subtype inclusion map) is linearly independent over $R$ if and only if the identity function restricted to $s$ is linearly independent over $R$. In other words, the vectors in $s$ are linearly independent if and only if the only linear combination of elements of $s$ that equals zero is the trivial one with all coefficients zero.

linearIndependent_comp_subtype_iff theorem

: LinearIndependent R (v ∘ Subtype.val : s → M) ↔ LinearIndepOn R v s

Full source

theorem linearIndependent_comp_subtype_iff :
    LinearIndependentLinearIndependent R (v ∘ Subtype.val : s → M) ↔ LinearIndepOn R v s := Iff.rfl

Linear Independence of Subtype Composition vs. Restriction to Subset

Informal description

Let $R$ be a ring, $M$ an $R$-module, $v : \iota \to M$ a family of vectors, and $s \subseteq \iota$ a subset. The composition $v \circ \text{Subtype.val} : s \to M$ is linearly independent over $R$ if and only if the family $v$ is linearly independent on $s$ (i.e., $\text{LinearIndepOn}_R v s$ holds).

LinearIndependent.comp theorem

(h : LinearIndependent R v) (f : ι' → ι) (hf : Injective f) : LinearIndependent R (v ∘ f)

Full source

/-- A subfamily of a linearly independent family (i.e., a composition with an injective map) is a
linearly independent family. -/
theorem LinearIndependent.comp (h : LinearIndependent R v) (f : ι' → ι) (hf : Injective f) :
    LinearIndependent R (v ∘ f) := by
  simpa [comp_def] using Injective.comp h (Finsupp.mapDomain_injective hf)

Linear Independence is Preserved Under Injective Composition

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. If $v$ is linearly independent over $R$ and $f : \iota' \to \iota$ is an injective function, then the composition $v \circ f : \iota' \to M$ is also linearly independent over $R$.

linearIndependent_iffₛ theorem

 : LinearIndependent R v ↔ ∀ l₁ l₂, Finsupp.linearCombination R v l₁ = Finsupp.linearCombination R v l₂ → l₁ = l₂

Full source

theorem linearIndependent_iffₛ :
    LinearIndependentLinearIndependent R v ↔
      ∀ l₁ l₂, Finsupp.linearCombination R v l₁ = Finsupp.linearCombination R v l₂ → l₁ = l₂ :=
  Iff.rfl

Linear Independence via Injectivity of Linear Combination Map

Informal description

A family of vectors $v : \iota \to M$ is linearly independent over a ring $R$ if and only if the linear combination map $\text{Finsupp.linearCombination}_R v : (\iota \to_{\text{f}} R) \to M$ is injective. That is, for any two finitely supported functions $l_1, l_2 : \iota \to_{\text{f}} R$, if $\sum_{i} l_1(i) \cdot v(i) = \sum_{i} l_2(i) \cdot v(i)$, then $l_1 = l_2$.

linearIndependent_iff'ₛ theorem

 : LinearIndependent R v ↔ ∀ s : Finset ι, ∀ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Full source

theorem linearIndependent_iff'ₛ :
    LinearIndependentLinearIndependent R v ↔
      ∀ s : Finset ι, ∀ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i :=
  linearIndependent_iffₛ.trans
    ⟨fun hv s f g eq i his ↦ by
      have h :=
        hv (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i)) <| by
          simpa only [map_sum, Finsupp.linearCombination_single] using eq
      have (f : ι → R) : f i = (∑ j ∈ s, Finsupp.single j (f j)) i :=
        calc
          f i = (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single i (f i)) := by
            { rw [Finsupp.lapply_apply, Finsupp.single_eq_same] }
          _ = ∑ j ∈ s, (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single j (f j)) :=
            Eq.symm <|
              Finset.sum_eq_single i
                (fun j _hjs hji => by rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne hji])
                fun hnis => hnis.elim his
          _ = (∑ j ∈ s, Finsupp.single j (f j)) i := (map_sum ..).symm
      rw [this f, this g, h],
      fun hv f g hl ↦
      Finsupp.ext fun _ ↦ by
        classical
        refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
        · rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;>
            rintro i - hi <;> rw [Finsupp.not_mem_support_iff.mp hi, zero_smul]
        · contrapose! hni
          simp_rw [not_mem_union, Finsupp.not_mem_support_iff] at hni
          rw [hni.1, hni.2]⟩

Linear Independence via Equality of Finite Linear Combinations

Informal description

A family of vectors $v : \iota \to M$ is linearly independent over a ring $R$ if and only if for every finite subset $s \subseteq \iota$ and any two functions $f, g : \iota \to R$, the equality $\sum_{i \in s} f(i) \cdot v(i) = \sum_{i \in s} g(i) \cdot v(i)$ implies $f(i) = g(i)$ for all $i \in s$.

linearIndependent_iff''ₛ theorem

 :
  LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i, f i = g i

Full source

theorem linearIndependent_iff''ₛ :
    LinearIndependentLinearIndependent R v ↔
      ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) →
        ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i, f i = g i := by
  classical
  exact linearIndependent_iff'ₛ.trans
    ⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his,
      fun H s f g eq i hi ↦ by
      convert
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
      exact (if_pos hi).symm⟩

Linear Independence via Equality of Finite Linear Combinations with Extended Agreement

Informal description

A family of vectors $v : \iota \to M$ is linearly independent over a ring $R$ if and only if for every finite subset $s \subseteq \iota$ and any two functions $f, g : \iota \to R$ that agree outside $s$, the equality $\sum_{i \in s} f(i) \cdot v(i) = \sum_{i \in s} g(i) \cdot v(i)$ implies $f(i) = g(i)$ for all $i \in \iota$.

not_linearIndependent_iffₛ theorem

 : ¬LinearIndependent R v ↔ ∃ s : Finset ι, ∃ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Full source

theorem not_linearIndependent_iffₛ :
    ¬LinearIndependent R v¬LinearIndependent R v ↔ ∃ s : Finset ι,
      ∃ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i := by
  rw [linearIndependent_iff'ₛ]
  simp only [exists_prop, not_forall]

Negation of Linear Independence via Finite Linear Combinations

Informal description

A family of vectors $v : \iota \to M$ is *not* linearly independent over a ring $R$ if and only if there exists a finite subset $s \subseteq \iota$ and two functions $f, g : \iota \to R$ such that $\sum_{i \in s} f(i) \cdot v(i) = \sum_{i \in s} g(i) \cdot v(i)$ but $f(i) \neq g(i)$ for some $i \in s$.

Fintype.linearIndependent_iffₛ theorem

 [Fintype ι] : LinearIndependent R v ↔ ∀ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i → ∀ i, f i = g i

Full source

theorem Fintype.linearIndependent_iffₛ [Fintype ι] :
    LinearIndependentLinearIndependent R v ↔ ∀ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i → ∀ i, f i = g i := by
  simp_rw [linearIndependent_iff_injective_fintypeLinearCombination,
    Injective, Fintype.linearCombination_apply, funext_iff]

Linear Independence Criterion for Finite Index Sets

Informal description

For a finite indexing type $\iota$, a family of vectors $v : \iota \to M$ is linearly independent over $R$ if and only if for any two functions $f, g : \iota \to R$, the equality $\sum_{i \in \iota} f(i) \cdot v(i) = \sum_{i \in \iota} g(i) \cdot v(i)$ implies $f(i) = g(i)$ for all $i \in \iota$.

Fintype.not_linearIndependent_iffₛ theorem

 [Fintype ι] : ¬LinearIndependent R v ↔ ∃ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i ∧ ∃ i, f i ≠ g i

Full source

theorem Fintype.not_linearIndependent_iffₛ [Fintype ι] :
    ¬LinearIndependent R v¬LinearIndependent R v ↔ ∃ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i ∧ ∃ i, f i ≠ g i := by
  simpa using not_iff_not.2 Fintype.linearIndependent_iffₛ

Negation of Linear Independence Criterion for Finite Index Sets

Informal description

For a finite indexing type $\iota$, a family of vectors $v : \iota \to M$ is *not* linearly independent over $R$ if and only if there exist two functions $f, g : \iota \to R$ such that $\sum_{i \in \iota} f(i) \cdot v(i) = \sum_{i \in \iota} g(i) \cdot v(i)$ but $f(i) \neq g(i)$ for some $i \in \iota$.

linearIndependent_iff_finset_linearIndependent theorem

: LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ (Subtype.val : s → ι))

Full source

/-- A family is linearly independent if and only if all of its finite subfamily is
linearly independent. -/
theorem linearIndependent_iff_finset_linearIndependent :
    LinearIndependentLinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ (Subtype.val : s → ι)) :=
  ⟨fun H _ ↦ H.comp _ Subtype.val_injective, fun H ↦ linearIndependent_iff'ₛ.2 fun s f g eq i hi ↦
    Fintype.linearIndependent_iffₛ.1 (H s) (f ∘ Subtype.val) (g ∘ Subtype.val)
      (by simpa only [← s.sum_coe_sort] using eq) ⟨i, hi⟩⟩

Finite Subset Characterization of Linear Independence

Informal description

A family of vectors $v : \iota \to M$ is linearly independent over a ring $R$ if and only if for every finite subset $s \subseteq \iota$, the restricted family $v|_s$ is linearly independent over $R$.

LinearIndependent.of_comp theorem

(f : M →ₗ[R] M') (hfv : LinearIndependent R (f ∘ v)) : LinearIndependent R v

Full source

/-- If the image of a family of vectors under a linear map is linearly independent, then so is
the original family. -/
theorem LinearIndependent.of_comp (f : M →ₗ[R] M') (hfv : LinearIndependent R (f ∘ v)) :
    LinearIndependent R v := by
  rw [LinearIndependent, Finsupp.linearCombination_linear_comp, LinearMap.coe_comp] at hfv
  exact hfv.of_comp

Linear Independence Preserved Under Precomposition with Linear Map

Informal description

Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a family of vectors in $M$. If there exists a linear map $f : M \to M'$ such that the composition $f \circ v : \iota \to M'$ is linearly independent over $R$, then the original family $v$ is also linearly independent over $R$.

LinearIndepOn.of_comp theorem

(f : M →ₗ[R] M') (hfv : LinearIndepOn R (f ∘ v) s) : LinearIndepOn R v s

Full source

theorem LinearIndepOn.of_comp (f : M →ₗ[R] M') (hfv : LinearIndepOn R (f ∘ v) s) :
    LinearIndepOn R v s :=
  LinearIndependent.of_comp f hfv

Linear Independence on Subset Preserved Under Precomposition with Linear Map

Informal description

Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a family of vectors in $M$. Given a subset $s \subseteq \iota$ and a linear map $f : M \to M'$, if the composition $f \circ v : \iota \to M'$ is linearly independent on $s$ over $R$, then the original family $v$ is also linearly independent on $s$ over $R$.

LinearMap.linearIndependent_iff_of_injOn theorem

 (f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (Set.range v))) : LinearIndependent R (f ∘ v) ↔ LinearIndependent R v

Full source

/-- If `f` is a linear map injective on the span of the range of `v`, then the family `f ∘ v`
is linearly independent if and only if the family `v` is linearly independent.
See `LinearMap.linearIndependent_iff_of_disjoint` for the version with `Set.InjOn` replaced
by `Disjoint` when working over a ring. -/
protected theorem LinearMap.linearIndependent_iff_of_injOn (f : M →ₗ[R] M')
    (hf_inj : Set.InjOn f (span R (Set.range v))) :
    LinearIndependentLinearIndependent R (f ∘ v) ↔ LinearIndependent R v := by
  simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp]
  rw [hf_inj.injective_iff]
  rw [← Finsupp.range_linearCombination, LinearMap.range_coe]

Linear Independence Preservation Under Injective Linear Maps on Span

Informal description

Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a family of vectors in $M$. Given a linear map $f : M \to M'$ that is injective on the span of the range of $v$, the family $f \circ v$ is linearly independent over $R$ if and only if the family $v$ is linearly independent over $R$.

LinearMap.linearIndepOn_iff_of_injOn theorem

(f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (v '' s))) : LinearIndepOn R (f ∘ v) s ↔ LinearIndepOn R v s

Full source

protected theorem LinearMap.linearIndepOn_iff_of_injOn (f : M →ₗ[R] M')
    (hf_inj : Set.InjOn f (span R (v '' s))) :
    LinearIndepOnLinearIndepOn R (f ∘ v) s ↔ LinearIndepOn R v s :=
  f.linearIndependent_iff_of_injOn (by rwa [← image_eq_range]) (v := fun i : s ↦ v i)

Linear Independence on Subset Preserved Under Injective Linear Maps on Span

Informal description

Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a family of vectors. Given a subset $s \subseteq \iota$ and a linear map $f : M \to M'$ that is injective on the span of $\{v_i\}_{i \in s}$, the family $f \circ v$ is linearly independent on $s$ over $R$ if and only if the family $v$ is linearly independent on $s$ over $R$.

linearIndependent_of_subsingleton theorem

[Subsingleton R] : LinearIndependent R v

Full source

@[nontriviality]
theorem linearIndependent_of_subsingleton [Subsingleton R] : LinearIndependent R v :=
  linearIndependent_iffₛ.2 fun _l _l' _hl => Subsingleton.elim _ _

Linear Independence in Subsingleton Rings

Informal description

If the ring $R$ is a subsingleton (i.e., has at most one element), then any family of vectors $v : \iota \to M$ is linearly independent over $R$.

LinearIndepOn.of_subsingleton theorem

[Subsingleton R] : LinearIndepOn R v s

Full source

@[nontriviality]
theorem LinearIndepOn.of_subsingleton [Subsingleton R] : LinearIndepOn R v s :=
  linearIndependent_of_subsingleton

Linear Independence on Subsets for Subsingleton Rings

Informal description

For any subset $s$ of the index set $\iota$ and any family of vectors $v : \iota \to M$ over a ring $R$, if $R$ is a subsingleton (i.e., has at most one element), then the vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$.

linearIndependent_equiv theorem

(e : ι ≃ ι') {f : ι' → M} : LinearIndependent R (f ∘ e) ↔ LinearIndependent R f

Full source

theorem linearIndependent_equiv (e : ι ≃ ι') {f : ι' → M} :
    LinearIndependentLinearIndependent R (f ∘ e) ↔ LinearIndependent R f :=
  ⟨fun h ↦ comp_id f ▸ e.self_comp_symm ▸ h.comp _ e.symm.injective,
    fun h ↦ h.comp _ e.injective⟩

Linear Independence is Preserved Under Index Equivalence: $f \circ e$ is linearly independent iff $f$ is

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $f : \iota' \to M$ a family of vectors in $M$. For any equivalence (bijection) $e : \iota \simeq \iota'$ between index types, the family $f \circ e : \iota \to M$ is linearly independent over $R$ if and only if $f$ is linearly independent over $R$.

linearIndependent_equiv' theorem

(e : ι ≃ ι') {f : ι' → M} {g : ι → M} (h : f ∘ e = g) : LinearIndependent R g ↔ LinearIndependent R f

Full source

theorem linearIndependent_equiv' (e : ι ≃ ι') {f : ι' → M} {g : ι → M} (h : f ∘ e = g) :
    LinearIndependentLinearIndependent R g ↔ LinearIndependent R f :=
  h ▸ linearIndependent_equiv e

Linear Independence Equivalence under Index Bijection: $g$ independent iff $f$ independent when $f \circ e = g$

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $f : \iota' \to M$ and $g : \iota \to M$ be families of vectors in $M$. Given an equivalence (bijection) $e : \iota \simeq \iota'$ between index types such that $f \circ e = g$, the family $g$ is linearly independent over $R$ if and only if $f$ is linearly independent over $R$.

linearIndepOn_equiv theorem

(e : ι ≃ ι') {f : ι' → M} {s : Set ι} : LinearIndepOn R (f ∘ e) s ↔ LinearIndepOn R f (e '' s)

Full source

theorem linearIndepOn_equiv (e : ι ≃ ι') {f : ι' → M} {s : Set ι} :
    LinearIndepOnLinearIndepOn R (f ∘ e) s ↔ LinearIndepOn R f (e '' s) :=
  linearIndependent_equiv' (e.image s) <| by simp [funext_iff]

Linear Independence Equivalence for Restricted Families under Index Bijection

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $f : \iota' \to M$ a family of vectors in $M$. Given an equivalence (bijection) $e : \iota \simeq \iota'$ between index types and a subset $s \subseteq \iota$, the restricted family $(f \circ e) \restriction s$ is linearly independent over $R$ if and only if the family $f \restriction e(s)$ is linearly independent over $R$.

linearIndepOn_univ theorem

: LinearIndepOn R v univ ↔ LinearIndependent R v

Full source

@[simp]
theorem linearIndepOn_univ : LinearIndepOnLinearIndepOn R v univ ↔ LinearIndependent R v :=
  linearIndependent_equiv' (Equiv.Set.univ ι) rfl

Linear Independence on Universal Set is Equivalent to Global Linear Independence

Informal description

For a family of vectors $v : \iota \to M$ over a ring $R$, the vectors are linearly independent on the universal set $\text{univ} = \iota$ if and only if the entire family $v$ is linearly independent over $R$.

linearIndepOn_iff_image theorem

{ι} {s : Set ι} {f : ι → M} (hf : Set.InjOn f s) : LinearIndepOn R f s ↔ LinearIndepOn R id (f '' s)

Full source

theorem linearIndepOn_iff_image {ι} {s : Set ι} {f : ι → M} (hf : Set.InjOn f s) :
    LinearIndepOnLinearIndepOn R f s ↔ LinearIndepOn R id (f '' s) :=
  linearIndependent_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

Linear Independence of a Family vs. Its Image Under an Injective Restriction

Informal description

Let $R$ be a ring, $M$ an $R$-module, $\iota$ a type, $s \subseteq \iota$ a subset, and $f : \iota \to M$ a family of vectors in $M$. If $f$ is injective on $s$, then the family $\{f(i)\}_{i \in s}$ is linearly independent over $R$ if and only if the family $\{x\}_{x \in f(s)}$ (where $f(s) = \{f(i) \mid i \in s\}$) is linearly independent over $R$ when viewed as the identity map on $f(s)$.

linearIndepOn_range_iff theorem

 {ι} {f : ι → ι'} (hf : Injective f) (g : ι' → M) : LinearIndepOn R g (range f) ↔ LinearIndependent R (g ∘ f)

Full source

theorem linearIndepOn_range_iff {ι} {f : ι → ι'} (hf : Injective f) (g : ι' → M) :
    LinearIndepOnLinearIndepOn R g (range f) ↔ LinearIndependent R (g ∘ f) :=
  Iff.symm <| linearIndependent_equiv' (Equiv.ofInjective f hf) rfl

Linear Independence on Range vs. Composition: $g$ independent on $\text{range}(f)$ iff $g \circ f$ independent

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $g : \iota' \to M$ a family of vectors in $M$. Given an injective function $f : \iota \to \iota'$, the family $g$ is linearly independent on the range of $f$ if and only if the composition $g \circ f : \iota \to M$ is linearly independent.

linearIndepOn_id_range_iff theorem

{ι} {f : ι → M} (hf : Injective f) : LinearIndepOn R id (range f) ↔ LinearIndependent R f

Full source

theorem linearIndepOn_id_range_iff {ι} {f : ι → M} (hf : Injective f) :
    LinearIndepOnLinearIndepOn R id (range f) ↔ LinearIndependent R f :=
  linearIndepOn_range_iff hf id

Linear Independence of Identity on Range vs. Linear Independence of Family: $\text{id}$ independent on $\text{range}(f)$ iff $f$ independent

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $f : \iota \to M$ an injective function. The identity function on $M$ is linearly independent on the range of $f$ if and only if the family of vectors $f$ is linearly independent over $R$.

LinearIndependent.linearIndepOn_id theorem

(i : LinearIndependent R v) : LinearIndepOn R id (range v)

Full source

theorem LinearIndependent.linearIndepOn_id (i : LinearIndependent R v) :
    LinearIndepOn R id (range v) := by
  simpa using i.comp _ (rangeSplitting_injective v)

Linear Independence of Identity Function on Range of Linearly Independent Vectors

Informal description

If a family of vectors $v : \iota \to M$ is linearly independent over a ring $R$, then the identity function restricted to the range of $v$ is linearly independent on the range of $v$ over $R$. In other words, the set $\{v_i\}_{i \in \iota}$ is linearly independent when viewed as a subset of $M$.

LinearIndependent.linearIndepOn_id' theorem

(hv : LinearIndependent R v) {t : Set M} (ht : Set.range v = t) : LinearIndepOn R id t

Full source

/-- A version of `LinearIndependent.linearIndepOn_id` with the set range equality as a hypothesis.
-/
theorem LinearIndependent.linearIndepOn_id' (hv : LinearIndependent R v) {t : Set M}
    (ht : Set.range v = t) : LinearIndepOn R id t :=
  ht ▸ hv.linearIndepOn_id

Linear Independence of Identity Function on Range-Equal Subset

Informal description

Let $v : \iota \to M$ be a family of vectors in a module $M$ over a ring $R$. If $v$ is linearly independent over $R$ and $t$ is a subset of $M$ such that the range of $v$ equals $t$ (i.e., $\text{range } v = t$), then the identity function restricted to $t$ is linearly independent on $t$ over $R$.

linearIndepOn_iffₛ theorem

 :
  LinearIndepOn R v s ↔
    ∀ f ∈ Finsupp.supported R R s,
      ∀ g ∈ Finsupp.supported R R s, Finsupp.linearCombination R v f = Finsupp.linearCombination R v g → f = g

Full source

theorem linearIndepOn_iffₛ : LinearIndepOnLinearIndepOn R v s ↔
      ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s,
        Finsupp.linearCombination R v f = Finsupp.linearCombination R v g → f = g := by
  simp only [LinearIndepOn, linearIndependent_iffₛ, (· ∘ ·), Finsupp.mem_supported,
    Finsupp.linearCombination_apply, Set.subset_def, Finset.mem_coe]
  refine ⟨fun h l₁ h₁ l₂ h₂ eq ↦ (Finsupp.subtypeDomain_eq_iff h₁ h₂).1 <| h _ _ <|
    (Finsupp.sum_subtypeDomain_index h₁).trans eq ▸ (Finsupp.sum_subtypeDomain_index h₂).symm,
    fun h l₁ l₂ eq ↦ ?_⟩
  refine Finsupp.embDomain_injective (Embedding.subtype s) <| h _ ?_ _ ?_ ?_
  iterate 2 simpa using fun _ h _ ↦ h
  simp_rw [Finsupp.embDomain_eq_mapDomain]
  rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index] <;>
    intros <;> simp only [zero_smul, add_smul]

Characterization of Linear Independence via Linear Combination Equality

Informal description

A family of vectors $\{v_i\}_{i \in s}$ in a module $M$ over a ring $R$ is linearly independent on a subset $s \subseteq \iota$ if and only if for any two finitely supported functions $f, g \colon \iota \to R$ with support contained in $s$, the equality of linear combinations $\sum_{i \in s} f(i) \cdot v_i = \sum_{i \in s} g(i) \cdot v_i$ implies $f = g$.

linearDepOn_iff'ₛ theorem

 :
  ¬LinearIndepOn R v s ↔
    ∃ f g : ι →₀ R,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ Finsupp.linearCombination R v f = Finsupp.linearCombination R v g ∧ f ≠ g

Full source

/-- An indexed set of vectors is linearly dependent iff there are two distinct
`Finsupp.LinearCombination`s of the vectors with the same value. -/
theorem linearDepOn_iff'ₛ : ¬LinearIndepOn R v s¬LinearIndepOn R v s ↔
      ∃ f g : ι →₀ R, f ∈ Finsupp.supported R R s ∧ g ∈ Finsupp.supported R R s ∧
        Finsupp.linearCombination R v f = Finsupp.linearCombination R v g ∧ f ≠ g := by
  simp [linearIndepOn_iffₛ, and_left_comm]

Linear Dependence Criterion via Distinct Linear Combinations

Informal description

A family of vectors $\{v_i\}_{i \in s}$ indexed by a set $s$ is linearly dependent over a ring $R$ if and only if there exist two distinct finitely supported functions $f, g : \iota \to R$ with support in $s$ such that the linear combinations $\sum_{i \in s} f(i) v_i$ and $\sum_{i \in s} g(i) v_i$ are equal.

linearDepOn_iffₛ theorem

 :
  ¬LinearIndepOn R v s ↔
    ∃ f g : ι →₀ R,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = ∑ i ∈ g.support, g i • v i ∧ f ≠ g

Full source

/-- A version of `linearDepOn_iff'ₛ` with `Finsupp.linearCombination` unfolded. -/
theorem linearDepOn_iffₛ : ¬LinearIndepOn R v s¬LinearIndepOn R v s ↔
      ∃ f g : ι →₀ R, f ∈ Finsupp.supported R R s ∧ g ∈ Finsupp.supported R R s ∧
        ∑ i ∈ f.support, f i • v i = ∑ i ∈ g.support, g i • v i ∧ f ≠ g :=
  linearDepOn_iff'ₛ

Linear Dependence Criterion via Finite Linear Combinations

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ over a ring $R$ is linearly dependent on a subset $s \subseteq \iota$ if and only if there exist two distinct finitely supported functions $f, g : \iota \to R$ with support contained in $s$ such that the linear combinations $\sum_{i \in \text{supp}(f)} f(i) \cdot v_i$ and $\sum_{i \in \text{supp}(g)} g(i) \cdot v_i$ are equal.

linearIndependent_restrict_iff theorem

: LinearIndependent R (s.restrict v) ↔ LinearIndepOn R v s

Full source

theorem linearIndependent_restrict_iff :
    LinearIndependentLinearIndependent R (s.restrict v) ↔ LinearIndepOn R v s := Iff.rfl

Equivalence of Linear Independence for Restricted Family and Subset

Informal description

For a family of vectors $v : \iota \to M$ over a ring $R$ and a subset $s \subseteq \iota$, the restriction of $v$ to $s$ is linearly independent if and only if the vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$.

LinearIndepOn.linearIndependent_restrict theorem

(hs : LinearIndepOn R v s) : LinearIndependent R (s.restrict v)

Full source

theorem LinearIndepOn.linearIndependent_restrict (hs : LinearIndepOn R v s) :
    LinearIndependent R (s.restrict v) :=
  hs

Linear Independence Preserved Under Restriction to a Subset

Informal description

Given a family of vectors $v : \iota \to M$ over a ring $R$ and a subset $s \subseteq \iota$, if the vectors $\{v_i\}_{i \in s}$ are linearly independent (i.e., $\text{LinearIndepOn}_R v s$ holds), then the restricted family $(v \restriction s) : s \to M$ is linearly independent over $R$.

linearIndepOn_iff_linearCombinationOnₛ theorem

: LinearIndepOn R v s ↔ Injective (Finsupp.linearCombinationOn ι M R v s)

Full source

theorem linearIndepOn_iff_linearCombinationOnₛ :
    LinearIndepOnLinearIndepOn R v s ↔ Injective (Finsupp.linearCombinationOn ι M R v s) := by
  rw [← linearIndependent_restrict_iff]
  simp [LinearIndependent, Finsupp.linearCombination_restrict]

Linear Independence on Subset Equivalent to Injectivity of Linear Combination Map

Informal description

For a family of vectors $v : \iota \to M$ over a ring $R$ and a subset $s \subseteq \iota$, the vectors $\{v_i\}_{i \in s}$ are linearly independent if and only if the linear combination map $\text{Finsupp.linearCombinationOn}_{\iota M R} v s$ is injective. Here, the linear combination map sends a finitely supported function $f : s \to_{\text{f}} R$ to the sum $\sum_{i \in s} f(i) \cdot v(i)$.

LinearIndependent.linearCombinationEquiv definition

(hv : LinearIndependent R v) : (ι →₀ R) ≃ₗ[R] span R (range v)

Full source

/-- Canonical isomorphism between linear combinations and the span of linearly independent vectors.
-/
@[simps (config := { rhsMd := default }) symm_apply]
def LinearIndependent.linearCombinationEquiv (hv : LinearIndependent R v) :
    (ι →₀ R) ≃ₗ[R] span R (range v) := by
  refine LinearEquiv.ofBijective (LinearMap.codRestrict (span R (range v))
                                 (Finsupp.linearCombination R v) ?_) ⟨hv.codRestrict _, ?_⟩
  · simp_rw [← Finsupp.range_linearCombination]; exact fun c ↦ ⟨c, rfl⟩
  rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]

Linear combination equivalence for linearly independent vectors

Informal description

Given a linearly independent family of vectors $ v : \iota \to M $ over a ring $ R $, the linear combination equivalence $ \text{LinearIndependent.linearCombinationEquiv} $ is a linear isomorphism between the space of finitely supported functions $ \iota \to_{\text{f}} R $ and the span of the range of $ v $. Specifically, it maps a finitely supported function $ l $ to the linear combination $ \sum_{i \in \text{supp}(l)} l(i) \cdot v(i) $, and this map is bijective.

LinearIndependent.linearCombinationEquiv_apply_coe theorem

(hv : LinearIndependent R v) (l : ι →₀ R) : hv.linearCombinationEquiv l = Finsupp.linearCombination R v l

Full source

@[simp]
theorem LinearIndependent.linearCombinationEquiv_apply_coe (hv : LinearIndependent R v)
    (l : ι →₀ R) : hv.linearCombinationEquiv l = Finsupp.linearCombination R v l := rfl

Linear Combination Equivalence Maps to Linear Combination

Informal description

Given a linearly independent family of vectors $v : \iota \to M$ over a ring $R$ and a finitely supported function $l : \iota \to_{\text{f}} R$, the linear combination equivalence $\text{LinearIndependent.linearCombinationEquiv}$ maps $l$ to the linear combination $\sum_{i \in \text{supp}(l)} l(i) \cdot v(i)$.

LinearIndependent.repr definition

(hv : LinearIndependent R v) : span R (range v) →ₗ[R] ι →₀ R

Full source

/-- Linear combination representing a vector in the span of linearly independent vectors.

Given a family of linearly independent vectors, we can represent any vector in their span as
a linear combination of these vectors. These are provided by this linear map.
It is simply one direction of `LinearIndependent.linearCombinationEquiv`. -/
def LinearIndependent.repr (hv : LinearIndependent R v) : spanspan R (range v) →ₗ[R] ι →₀ R :=
  hv.linearCombinationEquiv.symm

Representation of a vector in the span of linearly independent vectors

Informal description

Given a linearly independent family of vectors $ v : \iota \to M $ over a ring $ R $, the linear map $ \text{repr} $ sends any vector $ x $ in the span of $ v $ to its unique representation as a linear combination of the vectors in $ v $. Specifically, for $ x \in \text{span}_R (\text{range } v) $, $ \text{repr } x $ is the unique finitely supported function $ l : \iota \to_{\text{f}} R $ such that $ x = \sum_{i \in \text{supp}(l)} l(i) \cdot v(i) $.

LinearIndependent.linearCombination_repr theorem

(x) : Finsupp.linearCombination R v (hv.repr x) = x

Full source

@[simp]
theorem LinearIndependent.linearCombination_repr (x) :
    Finsupp.linearCombination R v (hv.repr x) = x :=
  Subtype.ext_iff.1 (LinearEquiv.apply_symm_apply hv.linearCombinationEquiv x)

Linear Combination Representation Property for Linearly Independent Vectors

Informal description

For any vector $x$ in the span of a linearly independent family of vectors $v : \iota \to M$ over a ring $R$, the linear combination of $v$ with coefficients given by the representation of $x$ equals $x$ itself. That is, $\sum_{i \in \text{supp}(l)} l(i) \cdot v(i) = x$ where $l = \text{repr}(x)$ is the unique representation of $x$ as a linear combination of $v$.

LinearIndependent.linearCombination_comp_repr theorem

: (Finsupp.linearCombination R v).comp hv.repr = Submodule.subtype _

Full source

theorem LinearIndependent.linearCombination_comp_repr :
    (Finsupp.linearCombination R v).comp hv.repr = Submodule.subtype _ :=
  LinearMap.ext <| hv.linearCombination_repr

Composition of Linear Combination and Representation Maps Equals Inclusion for Linearly Independent Vectors

Informal description

Let $R$ be a ring and $M$ be an $R$-module. Given a linearly independent family of vectors $v : \iota \to M$, the composition of the linear combination map $\text{Finsupp.linearCombination}_R v$ with the representation map $\text{repr}$ equals the canonical inclusion map from $\text{span}_R (\text{range } v)$ into $M$. In other words, for any $x \in \text{span}_R (\text{range } v)$, we have $\sum_{i \in \text{supp}(\text{repr}(x))} \text{repr}(x)(i) \cdot v(i) = x$.

LinearIndependent.repr_ker theorem

: LinearMap.ker hv.repr = ⊥

Full source

theorem LinearIndependent.repr_ker : LinearMap.ker hv.repr = ⊥ := by
  rw [LinearIndependent.repr, LinearEquiv.ker]

Trivial Kernel of Representation Map for Linearly Independent Vectors

Informal description

For a linearly independent family of vectors $v : \iota \to M$ over a ring $R$, the kernel of the representation map $\operatorname{repr} : \operatorname{span}_R (\operatorname{range} v) \to \iota \to_{\text{f}} R$ is trivial, i.e., $\ker(\operatorname{repr}) = \bot$.

LinearIndependent.repr_range theorem

: LinearMap.range hv.repr = ⊤

Full source

theorem LinearIndependent.repr_range : LinearMap.range hv.repr = ⊤ := by
  rw [LinearIndependent.repr, LinearEquiv.range]

Range of Representation Map for Linearly Independent Vectors is Entire Finitely Supported Function Space

Informal description

For a linearly independent family of vectors $v : \iota \to M$ over a ring $R$, the range of the representation map $\text{repr} : \text{span}_R (\text{range } v) \to \iota \to_{\text{f}} R$ is the entire space of finitely supported functions $\iota \to_{\text{f}} R$. In other words, every finitely supported function can be obtained as the representation of some vector in the span of $v$.

LinearIndependent.repr_eq theorem

{l : ι →₀ R} {x : span R (range v)} (eq : Finsupp.linearCombination R v l = ↑x) : hv.repr x = l

Full source

theorem LinearIndependent.repr_eq {l : ι →₀ R} {x : span R (range v)}
    (eq : Finsupp.linearCombination R v l = ↑x) : hv.repr x = l := by
  have :
    ↑((LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l) =
      Finsupp.linearCombination R v l :=
    rfl
  have : (LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x := by
    rw [eq] at this
    exact Subtype.ext_iff.2 this
  rw [← LinearEquiv.symm_apply_apply hv.linearCombinationEquiv l]
  rw [← this]
  rfl

Uniqueness of Linear Combination Representation for Linearly Independent Vectors

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors that is linearly independent over $R$. For any finitely supported function $l : \iota \to_{\text{f}} R$ and any vector $x$ in the span of $v$, if the linear combination $\sum_{i \in \text{supp}(l)} l(i) \cdot v(i)$ equals $x$, then the representation of $x$ as a linear combination of $v$ is exactly $l$.

LinearIndependent.repr_eq_single theorem

(i) (x : span R (range v)) (hx : ↑x = v i) : hv.repr x = Finsupp.single i 1

Full source

theorem LinearIndependent.repr_eq_single (i) (x : span R (range v)) (hx : ↑x = v i) :
    hv.repr x = Finsupp.single i 1 := by
  apply hv.repr_eq
  simp [Finsupp.linearCombination_single, hx]

Representation of Basis Vector as Single Nonzero Coefficient

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a linearly independent family of vectors over $R$. For any index $i \in \iota$ and any vector $x$ in the span of $v$ such that $x = v_i$, the representation of $x$ as a linear combination of $v$ is given by the finitely supported function that takes the value $1$ at $i$ and $0$ elsewhere. In other words, $\text{repr}(x) = \text{single}_i 1$.

LinearIndependent.span_repr_eq theorem

[Nontrivial R] (x) : Span.repr R (Set.range v) x = (hv.repr x).equivMapDomain (Equiv.ofInjective _ hv.injective)

Full source

theorem LinearIndependent.span_repr_eq [Nontrivial R] (x) :
    Span.repr R (Set.range v) x =
      (hv.repr x).equivMapDomain (Equiv.ofInjective _ hv.injective) := by
  have p :
    (Span.repr R (Set.range v) x).equivMapDomain (Equiv.ofInjective _ hv.injective).symm =
      hv.repr x := by
    apply (LinearIndependent.linearCombinationEquiv hv).injective
    ext
    simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
      LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
      Span.finsupp_linearCombination_repr]
  ext ⟨_, ⟨i, rfl⟩⟩
  simp [← p]

Equality of Span Representations for Linearly Independent Vectors

Informal description

Let $R$ be a nontrivial ring, $M$ an $R$-module, and $v : \iota \to M$ a linearly independent family of vectors. For any vector $x$ in the span of $v$, the representation of $x$ in terms of the spanning set $\text{range}(v)$ equals the domain-remapped representation of $x$ in terms of the linearly independent family $v$, where the remapping is via the equivalence between $\iota$ and $\text{range}(v)$ induced by the injectivity of $v$. More precisely, for any $x \in \text{span}_R(\text{range}(v))$, we have: $$\text{Span.repr}_R(\text{range}(v))(x) = \text{equivMapDomain}(e, \text{hv.repr}(x))$$ where $e : \iota \simeq \text{range}(v)$ is the equivalence induced by the injectivity of $v$.

LinearIndependent.not_smul_mem_span theorem

(hv : LinearIndependent R v) (i : ι) (a : R) (ha : a • v i ∈ span R (v '' (univ \ { i }))) : a = 0

Full source

theorem LinearIndependent.not_smul_mem_span (hv : LinearIndependent R v) (i : ι) (a : R)
    (ha : a • v i ∈ span R (v '' (univ \ {i}))) : a = 0 := by
  rw [Finsupp.span_image_eq_map_linearCombination, mem_map] at ha
  rcases ha with ⟨l, hl, e⟩
  rw [linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])] at hl
  by_contra hn
  exact (not_mem_of_mem_diff (hl <| by simp [hn])) (mem_singleton _)

Linear Independence Implies Non-Trivial Scalar Coefficients Outside Span

Informal description

Let $R$ be a ring and $M$ an $R$-module. Given a linearly independent family of vectors $v : \iota \to M$, an index $i \in \iota$, and a scalar $a \in R$, if the scaled vector $a \cdot v_i$ lies in the span of the vectors $\{v_j \mid j \in \iota \setminus \{i\}\}$, then $a = 0$.

LinearIndependent.Maximal definition

 {ι : Type w} {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {v : ι → M}
  (_i : LinearIndependent R v) : Prop

Full source

/--
A linearly independent family is maximal if there is no strictly larger linearly independent family.
-/
@[nolint unusedArguments]
def LinearIndependent.Maximal {ι : Type w} {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M]
    [Module R M] {v : ι → M} (_i : LinearIndependent R v) : Prop :=
  ∀ (s : Set M) (_i' : LinearIndependent R ((↑) : s → M)) (_h : range v ≤ s), range v = s

Maximal linear independence

Informal description

A linearly independent family of vectors $ v : \iota \to M $ is called maximal if for any set $ s \subseteq M $ containing the range of $ v $, any linearly independent family of vectors in $ s $ must be equal to the range of $ v $. In other words, there is no strictly larger set of vectors in $ M $ that remains linearly independent.

LinearIndependent.maximal_iff theorem

 {ι : Type w} {R : Type u} [Semiring R] [Nontrivial R] {M : Type v} [AddCommMonoid M] [Module R M] {v : ι → M}
  (i : LinearIndependent R v) :
  i.Maximal ↔ ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j

Full source

/-- An alternative characterization of a maximal linearly independent family,
quantifying over types (in the same universe as `M`) into which the indexing family injects.
-/
theorem LinearIndependent.maximal_iff {ι : Type w} {R : Type u} [Semiring R] [Nontrivial R]
    {M : Type v} [AddCommMonoid M] [Module R M] {v : ι → M} (i : LinearIndependent R v) :
    i.Maximal ↔
      ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v),
        Surjective j := by
  constructor
  · rintro p κ w i' j rfl
    specialize p (range w) i'.linearIndepOn_id (range_comp_subset_range _ _)
    rw [range_comp, ← image_univ (f := w)] at p
    exact range_eq_univ.mp (image_injective.mpr i'.injective p)
  · intro p w i' h
    specialize
      p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
        (by
          ext
          simp)
    have q := congr_arg (fun s => ((↑) : w → M) '' s) p.range_eq
    dsimp at q
    rw [← image_univ, image_image] at q
    simpa using q

Maximal Linear Independence Characterization via Surjective Embeddings

Informal description

Let $R$ be a nontrivial semiring and $M$ an $R$-module. A linearly independent family of vectors $v : \iota \to M$ is maximal if and only if for every type $\kappa$ in the same universe as $M$ and every linearly independent family $w : \kappa \to M$, any injective map $j : \iota \to \kappa$ satisfying $w \circ j = v$ must be surjective.

linearIndependent_iff_ker theorem

: LinearIndependent R v ↔ LinearMap.ker (Finsupp.linearCombination R v) = ⊥

Full source

theorem linearIndependent_iff_ker :
    LinearIndependentLinearIndependent R v ↔ LinearMap.ker (Finsupp.linearCombination R v) = ⊥ :=
  LinearMap.ker_eq_bot.symm

Linear independence is equivalent to trivial kernel of linear combination map

Informal description

A family of vectors $v : \iota \to M$ is linearly independent over a semiring $R$ if and only if the kernel of the linear combination map $\text{Finsupp.linearCombination}_R v : (\iota \to_{\text{f}} R) \to M$ is trivial (i.e., equal to the zero subspace $\bot$).

linearIndependent_iff theorem

: LinearIndependent R v ↔ ∀ l, Finsupp.linearCombination R v l = 0 → l = 0

Full source

theorem linearIndependent_iff :
    LinearIndependentLinearIndependent R v ↔ ∀ l, Finsupp.linearCombination R v l = 0 → l = 0 := by
  simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot']

Characterization of Linear Independence via Linear Combinations

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in a module $M$ over a semiring $R$ is linearly independent if and only if for every finitely supported function $l : \iota \to_{\text{f}} R$, the condition $\sum_{i \in \text{supp}(l)} l(i) \cdot v_i = 0$ implies $l = 0$.

linearIndependent_iff' theorem

: LinearIndependent R v ↔ ∀ s : Finset ι, ∀ g : ι → R, ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Full source

/-- A version of `linearIndependent_iff` where the linear combination is a `Finset` sum. -/
theorem linearIndependent_iff' :
    LinearIndependentLinearIndependent R v ↔
      ∀ s : Finset ι, ∀ g : ι → R, ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0 := by
  rw [linearIndependent_iff'ₛ]
  refine ⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩
  · convert h s f 0; simp_rw [Pi.zero_apply, zero_smul, Finset.sum_const_zero]
  · rw [← sub_eq_zero, ← Finset.sum_sub_distrib]
    convert h s (f - g) using 3 <;> simp only [Pi.sub_apply, sub_smul, sub_eq_zero]

Linear Independence via Vanishing Finite Linear Combinations

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in a module $M$ over a ring $R$ is linearly independent if and only if for every finite subset $s \subseteq \iota$ and every function $g : \iota \to R$, the condition $\sum_{i \in s} g(i) \cdot v_i = 0$ implies $g(i) = 0$ for all $i \in s$.

linearIndependent_iff'' theorem

 : LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ i, g i = 0

Full source

/-- A version of `linearIndependent_iff` where the linear combination is a `Finset` sum
of a function with support contained in the `Finset`. -/
theorem linearIndependent_iff'' :
    LinearIndependentLinearIndependent R v ↔
      ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ i, g i = 0 := by
  classical
  exact linearIndependent_iff'.trans
    ⟨fun H s g hg hv i => if his : i ∈ s then H s g hv i his else hg i his, fun H s g hg i hi => by
      convert
        H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) i
      exact (if_pos hi).symm⟩

Linear Independence via Vanishing Finite Linear Combinations with Vanishing Condition

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in a module $M$ over a ring $R$ is linearly independent if and only if for every finite subset $s \subseteq \iota$ and every function $g : \iota \to R$ that vanishes outside $s$, the condition $\sum_{i \in s} g(i) \cdot v_i = 0$ implies $g(i) = 0$ for all $i \in \iota$.

linearIndependent_add_smul_iff theorem

{c : ι → R} {i : ι} (h₀ : c i = 0) : LinearIndependent R (v + (c · • v i)) ↔ LinearIndependent R v

Full source

theorem linearIndependent_add_smul_iff {c : ι → R} {i : ι} (h₀ : c i = 0) :
    LinearIndependentLinearIndependent R (v + (c · • v i)) ↔ LinearIndependent R v := by
  simp [linearIndependent_iff_injective_finsuppLinearCombination,
    ← Finsupp.linearCombination_comp_addSingleEquiv i c h₀]

Linear independence preserved under adding scalar multiples of a fixed vector (when coefficient is zero at that vector)

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. For any function $c : \iota \to R$ and index $i \in \iota$ such that $c(i) = 0$, the family $(v + c \cdot v_i)$ is linearly independent over $R$ if and only if the original family $v$ is linearly independent over $R$. Here, $(v + c \cdot v_i)$ denotes the family where each vector $v_j$ is modified by adding $c(j) \cdot v_i$ (with $v_i$ being the $i$-th vector in the family $v$).

not_linearIndependent_iff theorem

 : ¬LinearIndependent R v ↔ ∃ s : Finset ι, ∃ g : ι → R, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Full source

theorem not_linearIndependent_iff :
    ¬LinearIndependent R v¬LinearIndependent R v ↔
      ∃ s : Finset ι, ∃ g : ι → R, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0 := by
  rw [linearIndependent_iff']
  simp only [exists_prop, not_forall]

Negation of Linear Independence via Non-Trivial Linear Combination

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in a module $M$ over a ring $R$ is not linearly independent if and only if there exists a finite subset $s \subseteq \iota$ and a function $g : \iota \to R$ such that the linear combination $\sum_{i \in s} g(i) \cdot v_i = 0$ and there exists some $i \in s$ with $g(i) \neq 0$.

Fintype.linearIndependent_iff theorem

[Fintype ι] : LinearIndependent R v ↔ ∀ g : ι → R, ∑ i, g i • v i = 0 → ∀ i, g i = 0

Full source

theorem Fintype.linearIndependent_iff [Fintype ι] :
    LinearIndependentLinearIndependent R v ↔ ∀ g : ι → R, ∑ i, g i • v i = 0 → ∀ i, g i = 0 := by
  refine
    ⟨fun H g => by simpa using linearIndependent_iff'.1 H Finset.univ g, fun H =>
      linearIndependent_iff''.2 fun s g hg hs i => H _ ?_ _⟩
  rw [← hs]
  refine (Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm
  rw [hg i hi, zero_smul]

Linear Independence Characterization for Finite Index Sets: $\sum_i g_i v_i = 0 \Rightarrow g_i = 0$ for all $i$

Informal description

Let $\iota$ be a finite type and $v : \iota \to M$ be a family of vectors in an $R$-module $M$. The family $v$ is linearly independent over $R$ if and only if for every function $g : \iota \to R$, the condition $\sum_{i \in \iota} g(i) \cdot v_i = 0$ implies $g(i) = 0$ for all $i \in \iota$.

Fintype.not_linearIndependent_iff theorem

[Fintype ι] : ¬LinearIndependent R v ↔ ∃ g : ι → R, ∑ i, g i • v i = 0 ∧ ∃ i, g i ≠ 0

Full source

theorem Fintype.not_linearIndependent_iff [Fintype ι] :
    ¬LinearIndependent R v¬LinearIndependent R v ↔ ∃ g : ι → R, ∑ i, g i • v i = 0 ∧ ∃ i, g i ≠ 0 := by
  simpa using not_iff_not.2 Fintype.linearIndependent_iff

Negation of Linear Independence via Non-Trivial Linear Combination for Finite Index Sets

Informal description

For a finite index set $\iota$ and a family of vectors $v : \iota \to M$ in an $R$-module $M$, the family $v$ is not linearly independent over $R$ if and only if there exists a function $g : \iota \to R$ such that $\sum_{i \in \iota} g(i) \cdot v_i = 0$ and there exists some $i \in \iota$ with $g(i) \neq 0$.

LinearMap.linearIndependent_iff_of_disjoint theorem

 (f : M →ₗ[R] M') (hf_inj : Disjoint (span R (Set.range v)) (LinearMap.ker f)) :
  LinearIndependent R (f ∘ v) ↔ LinearIndependent R v

Full source

/-- If the kernel of a linear map is disjoint from the span of a family of vectors,
then the family is linearly independent iff it is linearly independent after composing with
the linear map. -/
protected theorem LinearMap.linearIndependent_iff_of_disjoint (f : M →ₗ[R] M')
    (hf_inj : Disjoint (span R (Set.range v)) (LinearMap.ker f)) :
    LinearIndependentLinearIndependent R (f ∘ v) ↔ LinearIndependent R v :=
  f.linearIndependent_iff_of_injOn <| LinearMap.injOn_of_disjoint_ker le_rfl hf_inj

Linear Independence Equivalence Under Disjoint Kernel Condition

Informal description

Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a family of vectors. Given a linear map $f : M \to M'$ such that the kernel of $f$ is disjoint from the span of the range of $v$, the family $f \circ v$ is linearly independent over $R$ if and only if the family $v$ is linearly independent over $R$.

linearIndepOn_iff theorem

: LinearIndepOn R v s ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0

Full source

theorem linearIndepOn_iff : LinearIndepOnLinearIndepOn R v s ↔
      ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0 :=
  linearIndepOn_iffₛ.trans ⟨fun h l hl ↦ h l hl 0 (zero_mem _), fun h f hf g hg eq ↦
    sub_eq_zero.mp (h (f - g) (sub_mem hf hg) <| by rw [map_sub, eq, sub_self])⟩

Characterization of Linear Independence via Trivial Linear Combination

Informal description

A family of vectors $\{v_i\}_{i \in s}$ in a module $M$ over a ring $R$ is linearly independent on a subset $s \subseteq \iota$ if and only if for every finitely supported function $l : \iota \to R$ with support contained in $s$, the condition $\sum_{i \in s} l(i) \cdot v_i = 0$ implies $l = 0$.

linearDepOn_iff' theorem

 : ¬LinearIndepOn R v s ↔ ∃ f : ι →₀ R, f ∈ Finsupp.supported R R s ∧ Finsupp.linearCombination R v f = 0 ∧ f ≠ 0

Full source

/-- An indexed set of vectors is linearly dependent iff there is a nontrivial
`Finsupp.linearCombination` of the vectors that is zero. -/
theorem linearDepOn_iff' : ¬LinearIndepOn R v s¬LinearIndepOn R v s ↔
      ∃ f : ι →₀ R, f ∈ Finsupp.supported R R s ∧ Finsupp.linearCombination R v f = 0 ∧ f ≠ 0 := by
  simp [linearIndepOn_iff, and_left_comm]

Characterization of Linear Dependence via Nontrivial Linear Combination

Informal description

A family of vectors $\{v_i\}_{i \in s}$ indexed by a set $s \subseteq \iota$ is *linearly dependent* over a ring $R$ if and only if there exists a nontrivial finitely supported function $f : \iota \to R$ with support in $s$ such that the linear combination $\sum_{i \in s} f(i) \cdot v_i = 0$.

linearDepOn_iff theorem

 : ¬LinearIndepOn R v s ↔ ∃ f : ι →₀ R, f ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0

Full source

/-- A version of `linearDepOn_iff'` with `Finsupp.linearCombination` unfolded. -/
theorem linearDepOn_iff : ¬LinearIndepOn R v s¬LinearIndepOn R v s ↔
      ∃ f : ι →₀ R, f ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0 :=
  linearDepOn_iff'

Characterization of Linear Dependence via Finite Nontrivial Linear Combination

Informal description

A family of vectors $\{v_i\}_{i \in s}$ indexed by a subset $s \subseteq \iota$ is *linearly dependent* over a ring $R$ if and only if there exists a nontrivial finitely supported function $f : \iota \to R$ with support in $s$ such that the finite linear combination $\sum_{i \in \text{supp}(f)} f(i) \cdot v_i = 0$.

linearIndepOn_iff_disjoint theorem

: LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker <| Finsupp.linearCombination R v)

Full source

theorem linearIndepOn_iff_disjoint: LinearIndepOnLinearIndepOn R v s ↔
      Disjoint (Finsupp.supported R R s) (LinearMap.ker <| Finsupp.linearCombination R v) := by
  rw [linearIndepOn_iff, LinearMap.disjoint_ker]

Linear Independence via Disjointness of Support and Kernel

Informal description

A family of vectors $\{v_i\}_{i \in s}$ indexed by a subset $s \subseteq \iota$ is linearly independent over a ring $R$ if and only if the subspace of finitely supported functions with support in $s$ is disjoint from the kernel of the linear combination map $\sum_{i \in \iota} f(i) \cdot v_i$.

linearIndepOn_iff_linearCombinationOn theorem

: LinearIndepOn R v s ↔ (LinearMap.ker <| Finsupp.linearCombinationOn ι M R v s) = ⊥

Full source

theorem linearIndepOn_iff_linearCombinationOn :
    LinearIndepOnLinearIndepOn R v s ↔ (LinearMap.ker <| Finsupp.linearCombinationOn ι M R v s) = ⊥ :=
  linearIndepOn_iff_linearCombinationOnₛ.trans <|
    LinearMap.ker_eq_bot (M := Finsupp.supported R R s).symm

Linear Independence on Subset Equivalent to Trivial Kernel of Linear Combination Map

Informal description

A family of vectors $\{v_i\}_{i \in s}$ indexed by a subset $s \subseteq \iota$ is linearly independent over a ring $R$ if and only if the kernel of the linear combination map $\text{Finsupp.linearCombinationOn}_{\iota M R} v s$ is trivial, i.e., equal to the zero subspace $\{0\}$. Here, the linear combination map sends a finitely supported function $f : s \to_{\text{f}} R$ to the sum $\sum_{i \in s} f(i) \cdot v_i$.

linearIndepOn_iff' theorem

 : LinearIndepOn R v s ↔ ∀ (t : Finset ι) (g : ι → R), (t : Set ι) ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0

Full source

/-- A version of `linearIndepOn_iff` where the linear combination is a `Finset` sum. -/
lemma linearIndepOn_iff' : LinearIndepOnLinearIndepOn R v s ↔ ∀ (t : Finset ι) (g : ι → R), (t : Set ι) ⊆ s →
    ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0 := by
  classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, setOf_mem_eq, smul_eq_zero]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit

Finite Linear Independence Criterion on Subset of Indices

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in an $R$-module $M$ is linearly independent on a subset $s \subseteq \iota$ if and only if for every finite subset $t \subseteq s$ and every function $g : \iota \to R$, the condition $\sum_{i \in t} g(i) \cdot v_i = 0$ implies $g(i) = 0$ for all $i \in t$.

linearIndepOn_iff'' theorem

 :
  LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (t : Set ι) ⊆ s → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0

Full source

/-- A version of `linearIndepOn_iff` where the linear combination is a `Finset` sum
of a function with support contained in the `Finset`. -/
lemma linearIndepOn_iff'' : LinearIndepOnLinearIndepOn R v s ↔ ∀ (t : Finset ι) (g : ι → R), (t : Set ι) ⊆ s →
    (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0 := by
  classical
  exact linearIndepOn_iff'.trans ⟨fun h t g hts htg h0 ↦ h _ _ hts h0, fun h t g hts h0 ↦
    by simpa +contextual [h0] using h t (fun i ↦ if i ∈ t then g i else 0) hts⟩

Finite Support Linear Independence Criterion on Subset of Indices

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in an $R$-module $M$ is linearly independent on a subset $s \subseteq \iota$ if and only if for every finite subset $t \subseteq s$ and every function $g : \iota \to R$ that vanishes outside $t$, the condition $\sum_{i \in t} g(i) \cdot v_i = 0$ implies $g(i) = 0$ for all $i \in t$.

linearIndependent_iff_not_smul_mem_span theorem

: LinearIndependent R v ↔ ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ { i })) → a = 0

Full source

theorem linearIndependent_iff_not_smul_mem_span :
    LinearIndependentLinearIndependent R v ↔ ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0 :=
  ⟨fun hv ↦ hv.not_smul_mem_span, fun H =>
    linearIndependent_iff.2 fun l hl => by
      ext i; simp only [Finsupp.zero_apply]
      by_contra hn
      refine hn (H i _ ?_)
      refine (Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩
      · rw [Finsupp.mem_supported']
        intro j hj
        have hij : j = i :=
          Classical.not_not.1 fun hij : j ≠ i =>
            hj ((mem_diff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
        simp [hij]
      · simp [hl]⟩

Characterization of Linear Independence via Non-Trivial Scalar Coefficients Outside Span

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in an $R$-module $M$ is linearly independent if and only if for every index $i \in \iota$ and every scalar $a \in R$, if the scaled vector $a \cdot v_i$ lies in the span of the remaining vectors $\{v_j \mid j \in \iota \setminus \{i\}\}$, then $a = 0$.

linearIndependent_iff_not_mem_span theorem

: LinearIndependent K v ↔ ∀ i, v i ∉ span K (v '' (univ \ { i }))

Full source

theorem linearIndependent_iff_not_mem_span :
    LinearIndependentLinearIndependent K v ↔ ∀ i, v i ∉ span K (v '' (univ \ {i})) := by
  apply linearIndependent_iff_not_smul_mem_span.trans
  constructor
  · intro h i h_in_span
    apply one_ne_zero (h i 1 (by simp [h_in_span]))
  · intro h i a ha
    by_contra ha'
    exact False.elim (h _ ((smul_mem_iff _ ha').1 ha))

Linear independence characterization via non-membership in span of remaining vectors

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in a vector space over a division ring $K$ is linearly independent if and only if for every index $i \in \iota$, the vector $v_i$ does not lie in the span of the remaining vectors $\{v_j \mid j \in \iota \setminus \{i\}\}$.

linearIndepOn_iff_not_mem_span theorem

: LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ { i }))

Full source

lemma linearIndepOn_iff_not_mem_span :
    LinearIndepOnLinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i})) := by
  rw [LinearIndepOn, linearIndependent_iff_not_mem_span, ← Function.comp_def]
  simp_rw [Set.image_comp]
  simp [Set.image_diff Subtype.val_injective]

Characterization of Linear Independence on Subset via Non-Membership in Span of Remaining Vectors

Informal description

A family of vectors $\{v_i\}_{i \in \iota}$ in a vector space over a division ring $K$ is linearly independent on a subset $s \subseteq \iota$ if and only if for every index $i \in s$, the vector $v_i$ does not lie in the span of the remaining vectors $\{v_j \mid j \in s \setminus \{i\}\}$.

Mathlib.LinearAlgebra.LinearIndependent.Defs

Main definitions

Main results

Implementation notes

TODO

Tags