Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Fintype.linearIndependent_iff'ₛ theorem

 [Fintype ι] [DecidableEq ι] :
  LinearIndependent R v ↔ Injective (LinearMap.lsum R (fun _ ↦ R) ℕ fun i ↦ LinearMap.id.smulRight (v i))

Full source

/-- A finite family of vectors `v i` is linear independent iff the linear map that sends
`c : ι → R` to `∑ i, c i • v i` is injective. -/
theorem Fintype.linearIndependent_iff'ₛ [Fintype ι] [DecidableEq ι] :
    LinearIndependentLinearIndependent R v ↔
      Injective (LinearMap.lsum R (fun _ ↦ R) ℕ fun i ↦ LinearMap.id.smulRight (v i)) := by
  simp [Fintype.linearIndependent_iffₛ, Injective, funext_iff]

Linear independence via injectivity of linear combination map for finite families

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $\iota$ a finite index set with decidable equality. A family of vectors $v : \iota \to M$ is linearly independent over $R$ if and only if the linear map \[ \sum_{i \in \iota} c_i \cdot v_i \] is injective as a function of the coefficients $c : \iota \to R$. Here, the map sends a coefficient vector $c$ to the linear combination $\sum_{i \in \iota} c_i v_i$.

LinearIndependent.pair_iffₛ theorem

 {x y : M} : LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Full source

lemma LinearIndependent.pair_iffₛ {x y : M} :
    LinearIndependentLinearIndependent R ![x, y] ↔
      ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t' := by
  simp [Fintype.linearIndependent_iffₛ, Fin.forall_fin_two, ← FinVec.forall_iff]; rfl

Linear Independence Criterion for Pairs of Vectors

Informal description

For any two vectors $x$ and $y$ in an $R$-module $M$, the family of vectors $[x, y]$ is linearly independent over $R$ if and only if for all scalars $s, t, s', t' \in R$, the equality $s x + t y = s' x + t' y$ implies $s = s'$ and $t = t'$.

linearIndepOn_iUnion_of_directed theorem

 {η : Type*} {s : η → Set ι} (hs : Directed (· ⊆ ·) s) (h : ∀ i, LinearIndepOn R v (s i)) : LinearIndepOn R v (⋃ i, s i)

Full source

theorem linearIndepOn_iUnion_of_directed {η : Type*} {s : η → Set ι} (hs : Directed (· ⊆ ·) s)
    (h : ∀ i, LinearIndepOn R v (s i)) : LinearIndepOn R v (⋃ i, s i) := by
  by_cases hη : Nonempty η
  · refine linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_
    rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
    rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
    exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
  · refine (linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_
    rintro _ ⟨_, ⟨i, _⟩, _⟩
    exact hη ⟨i⟩

Linear Independence Preserved Under Directed Union of Index Sets

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. Given a directed family of subsets $\{s_i\}_{i \in \eta}$ of $\iota$ (i.e., for any $i,j \in \eta$, there exists $k \in \eta$ such that $s_i \subseteq s_k$ and $s_j \subseteq s_k$), if for each $i \in \eta$ the vectors $\{v_j\}_{j \in s_i}$ are linearly independent over $R$, then the vectors $\{v_j\}_{j \in \bigcup_{i \in \eta} s_i}$ are also linearly independent over $R$.

linearIndepOn_sUnion_of_directed theorem

 {s : Set (Set ι)} (hs : DirectedOn (· ⊆ ·) s) (h : ∀ a ∈ s, LinearIndepOn R v a) : LinearIndepOn R v (⋃₀ s)

Full source

theorem linearIndepOn_sUnion_of_directed {s : Set (Set ι)} (hs : DirectedOn (· ⊆ ·) s)
    (h : ∀ a ∈ s, LinearIndepOn R v a) : LinearIndepOn R v (⋃₀ s) := by
  rw [sUnion_eq_iUnion]
  exact linearIndepOn_iUnion_of_directed hs.directed_val (by simpa using h)

Linear Independence Preserved Under Directed Union of Sets of Vectors

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. Given a directed family of subsets $\{s_i\}_{i \in \eta}$ of $\iota$ (i.e., for any $s_i, s_j \in \eta$, there exists $s_k \in \eta$ such that $s_i \subseteq s_k$ and $s_j \subseteq s_k$), if for each $s_i \in \eta$ the vectors $\{v_j\}_{j \in s_i}$ are linearly independent over $R$, then the vectors $\{v_j\}_{j \in \bigcup_{s_i \in \eta} s_i}$ are also linearly independent over $R$.

linearIndepOn_biUnion_of_directed theorem

 {η} {s : Set η} {t : η → Set ι} (hs : DirectedOn (t ⁻¹'o (· ⊆ ·)) s) (h : ∀ a ∈ s, LinearIndepOn R v (t a)) :
  LinearIndepOn R v (⋃ a ∈ s, t a)

Full source

theorem linearIndepOn_biUnion_of_directed {η} {s : Set η} {t : η → Set ι}
    (hs : DirectedOn (t ⁻¹'o (· ⊆ ·)) s) (h : ∀ a ∈ s, LinearIndepOn R v (t a)) :
    LinearIndepOn R v (⋃ a ∈ s, t a) := by
  rw [biUnion_eq_iUnion]
  exact linearIndepOn_iUnion_of_directed (directed_comp.2 <| hs.directed_val) (by simpa using h)

Linear Independence Preserved Under Directed Bounded Union of Index Sets

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. Given a set $s$ of indices of type $\eta$ and a family of subsets $t : \eta \to \text{Set } \iota$ such that the preimage of the subset relation under $t$ is directed on $s$, if for every $a \in s$ the vectors $\{v_i\}_{i \in t(a)}$ are linearly independent over $R$, then the vectors $\{v_i\}_{i \in \bigcup_{a \in s} t(a)}$ are also linearly independent over $R$.

LinearIndependent.iSupIndep_span_singleton theorem

(hv : LinearIndependent R v) : iSupIndep fun i => R ∙ v i

Full source

/-- See also `iSupIndep_iff_linearIndependent_of_ne_zero`. -/
theorem LinearIndependent.iSupIndep_span_singleton (hv : LinearIndependent R v) :
    iSupIndep fun i => R ∙ v i := by
  refine iSupIndep_def.mp fun i => ?_
  rw [disjoint_iff_inf_le]
  intro m hm
  simp only [mem_inf, mem_span_singleton, iSup_subtype'] at hm
  rw [← span_range_eq_iSup] at hm
  obtain ⟨⟨r, rfl⟩, hm⟩ := hm
  suffices r = 0 by simp [this]
  apply hv.not_smul_mem_span i
  convert hm
  ext
  simp

Independence of Cyclic Submodules Generated by a Linearly Independent Family

Informal description

Let $R$ be a ring and $M$ an $R$-module. If a family of vectors $v : \iota \to M$ is linearly independent over $R$, then the family of cyclic submodules $\{R \cdot v_i\}_{i \in \iota}$ is independent in the sense that their supremum (join) in the submodule lattice satisfies the condition of being independent. More precisely, for any finite subset $s \subseteq \iota$, the intersection of $\bigsqcup_{i \in s} (R \cdot v_i)$ with $\bigsqcup_{i \notin s} (R \cdot v_i)$ is the zero submodule.

linearIndependent_inl_union_inr' theorem

 {v : ι → M} {v' : ι' → M'} (hv : LinearIndependent R v) (hv' : LinearIndependent R v') :
  LinearIndependent R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v'))

Full source

theorem linearIndependent_inl_union_inr' {v : ι → M} {v' : ι' → M'}
    (hv : LinearIndependent R v) (hv' : LinearIndependent R v') :
    LinearIndependent R (Sum.elim (inlinl R M M' ∘ v) (inrinr R M M' ∘ v')) := by
  have : linearCombination R (Sum.elim (inlinl R M M' ∘ v) (inrinr R M M' ∘ v')) =
      .prodMap.prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (sumFinsuppLEquivProdFinsupp R).toLinearMap := by
    ext (_ | _) <;> simp [linearCombination_comapDomain]
  rw [LinearIndependent, this]
  simpa [LinearMap.coe_prodMap] using ⟨hv, hv'⟩

Linear Independence of Combined Left and Right Injections in Product Module

Informal description

Let $R$ be a ring, and let $M$ and $M'$ be $R$-modules. Given two families of vectors $v : \iota \to M$ and $v' : \iota' \to M'$ that are linearly independent over $R$, the combined family formed by the left injections of $v$ and the right injections of $v'$ into $M \times M'$ is also linearly independent over $R$. More precisely, if we define the combined family as: \[ w : \iota \sqcup \iota' \to M \times M' \] \[ w(i) = \begin{cases} (v(i), 0) & \text{if } i \in \iota, \\ (0, v'(j)) & \text{if } i = j \in \iota', \end{cases} \] then $w$ is linearly independent over $R$.

LinearIndependent.inl_union_inr theorem

 {s : Set M} {t : Set M'} (hs : LinearIndependent R (fun x => x : s → M))
  (ht : LinearIndependent R (fun x => x : t → M')) :
  LinearIndependent R (fun x => x : ↥(inl R M M' '' s ∪ inr R M M' '' t) → M × M')

Full source

theorem LinearIndependent.inl_union_inr {s : Set M} {t : Set M'}
    (hs : LinearIndependent R (fun x => x : s → M))
    (ht : LinearIndependent R (fun x => x : t → M')) :
    LinearIndependent R (fun x => x : ↥(inlinl R M M' '' sinl R M M' '' s ∪ inr R M M' '' t) → M × M') := by
  nontriviality R
  let e : s ⊕ ts ⊕ t ≃ ↥(inl R M M' '' s ∪ inr R M M' '' t) :=
    .ofBijective (Sum.elim (fun i ↦ ⟨_, .inl ⟨_, i.2, rfl⟩⟩) fun i ↦ ⟨_, .inr ⟨_, i.2, rfl⟩⟩)
      ⟨by rintro (_|_) (_|_) eq <;> simp [hs.ne_zero, ht.ne_zero] at eq <;> aesop,
        by rintro ⟨_, ⟨_, _, rfl⟩ | ⟨_, _, rfl⟩⟩ <;> aesop⟩
  refine (linearIndependent_equiv' e ?_).mp (linearIndependent_inl_union_inr' hs ht)
  ext (_ | _) <;> rfl

Linear Independence of Union of Left and Right Injected Sets in Product Module

Informal description

Let $R$ be a ring, and let $M$ and $M'$ be $R$-modules. Given two sets of vectors $s \subseteq M$ and $t \subseteq M'$ that are linearly independent over $R$, the union of the images of $s$ under the left injection $\text{inl} : M \to M \times M'$ and $t$ under the right injection $\text{inr} : M' \to M \times M'$ is also linearly independent over $R$. More precisely, the set $\text{inl}(s) \cup \text{inr}(t) \subseteq M \times M'$ is linearly independent, where $\text{inl}(x) = (x, 0)$ and $\text{inr}(y) = (0, y)$ for $x \in s$ and $y \in t$.

exists_maximal_linearIndepOn' theorem

(v : ι → M) : ∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ t : Set ι, s ⊆ t → (LinearIndepOn R v t) → s = t

Full source

/-- TODO : refactor to use `Maximal`. -/
theorem exists_maximal_linearIndepOn' (v : ι → M) :
    ∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ t : Set ι, s ⊆ t → (LinearIndepOn R v t) → s = t := by
  let indep : Set ι → Prop := fun s => LinearIndepOn R v s
  let X := { I : Set ι // indep I }
  let r : X → X → Prop := fun I J => I.1 ⊆ J.1
  have key : ∀ c : Set X, IsChain r c → indep (⋃ (I : X) (_ : I ∈ c), I) := by
    intro c hc
    dsimp [indep]
    rw [linearIndepOn_iffₛ]
    intro f hfsupp g hgsupp hsum
    rcases eq_empty_or_nonempty c with (rfl | hn)
    · rw [show f = 0 by simpa using hfsupp, show g = 0 by simpa using hgsupp]
    haveI : IsRefl X r := ⟨fun _ => Set.Subset.refl _⟩
    classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum
  have trans : Transitive r := fun I J K => Set.Subset.trans
  obtain ⟨⟨I, hli : indep I⟩, hmax : ∀ a, r ⟨I, hli⟩ a → r a ⟨I, hli⟩⟩ :=
    exists_maximal_of_chains_bounded
      (fun c hc => ⟨⟨⋃ I ∈ c, (I : Set ι), key c hc⟩, fun I => Set.subset_biUnion_of_mem⟩) @trans
  exact ⟨I, hli, fun J hsub hli => Set.Subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩

Existence of Maximal Linearly Independent Subset for Any Family of Vectors

Informal description

For any family of vectors $v \colon \iota \to M$ in a module $M$ over a ring $R$, there exists a maximal subset $s \subseteq \iota$ such that the restricted family $\{v_i\}_{i \in s}$ is linearly independent. Moreover, any strictly larger subset $t \supsetneq s$ is not linearly independent.

Fintype.linearIndependent_iff' theorem

 [Fintype ι] [DecidableEq ι] :
  LinearIndependent R v ↔ LinearMap.ker (LinearMap.lsum R (fun _ ↦ R) ℕ fun i ↦ LinearMap.id.smulRight (v i)) = ⊥

Full source

/-- A finite family of vectors `v i` is linear independent iff the linear map that sends
`c : ι → R` to `∑ i, c i • v i` has the trivial kernel. -/
theorem Fintype.linearIndependent_iff' [Fintype ι] [DecidableEq ι] :
    LinearIndependentLinearIndependent R v ↔
      LinearMap.ker (LinearMap.lsum R (fun _ ↦ R) ℕ fun i ↦ LinearMap.id.smulRight (v i)) = ⊥ := by
  simp [Fintype.linearIndependent_iff, LinearMap.ker_eq_bot', funext_iff]

Linear independence criterion via kernel triviality for finite families

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $\iota$ a finite type with decidable equality. A family of vectors $v : \iota \to M$ is linearly independent if and only if the kernel of the linear map \[ \sum_{i \in \iota} c_i \cdot v_i \quad \text{(where $c_i \in R$)} \] is trivial (i.e., equals $\bot$).

LinearIndepOn.pair_iff theorem

 {i j : ι} (f : ι → M) (hij : i ≠ j) : LinearIndepOn R f { i, j } ↔ ∀ c d : R, c • f i + d • f j = 0 → c = 0 ∧ d = 0

Full source

/-- `linearIndepOn_pair_iff` is a simpler version over fields. -/
lemma LinearIndepOn.pair_iff {i j : ι} (f : ι → M) (hij : i ≠ j) :
    LinearIndepOnLinearIndepOn R f {i,j} ↔ ∀ c d : R, c • f i + d • f j = 0 → c = 0 ∧ d = 0 := by
  classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]

Linear Independence Criterion for Vector Pairs: $\{f(i), f(j)\}$ is linearly independent if and only if $c \cdot f(i) + d \cdot f(j) = 0$ implies $c = d = 0$

Informal description

For any distinct indices $i \neq j$ and any family of vectors $f \colon \iota \to M$ in an $R$-module $M$, the vectors $\{f(i), f(j)\}$ are linearly independent on the set $\{i, j\}$ if and only if for all scalars $c, d \in R$, the equation $c \cdot f(i) + d \cdot f(j) = 0$ implies $c = 0$ and $d = 0$.

LinearIndependent.pair_iff theorem

: LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Full source

/-- Also see `LinearIndependent.pair_iff'` for a simpler version over fields. -/
lemma LinearIndependent.pair_iff :
    LinearIndependentLinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0 := by
  rw [← linearIndepOn_univ, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0,1} from rfl,
    Finset.coe_insert, Finset.coe_singleton, LinearIndepOn.pair_iff _ (by trivial)]
  simp

Linear independence criterion for vector pairs: $sx + ty = 0 \Rightarrow s = t = 0$

Informal description

For any two vectors $x$ and $y$ in an $R$-module $M$, the pair $\{x, y\}$ is linearly independent if and only if for all scalars $s, t \in R$, the equation $s \cdot x + t \cdot y = 0$ implies $s = 0$ and $t = 0$.

LinearIndependent.pair_symm_iff theorem

: LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Full source

lemma LinearIndependent.pair_symm_iff :
    LinearIndependentLinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x] := by
  suffices ∀ x y : M, LinearIndependent R ![x, y] → LinearIndependent R ![y, x] by tauto
  simp only [LinearIndependent.pair_iff]
  intro x y h s t
  specialize h t s
  rwa [add_comm, and_comm]

Symmetry of Linear Independence for Vector Pairs

Informal description

For any two vectors $x$ and $y$ in a module $M$ over a ring $R$, the family of vectors $[x, y]$ is linearly independent if and only if the family $[y, x]$ is linearly independent.

LinearIndependent.pair_neg_left_iff theorem

: LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y]

Full source

@[simp] lemma LinearIndependent.pair_neg_left_iff :
    LinearIndependentLinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y] := by
  rw [pair_iff, pair_iff]
  refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩ <;> simpa using h (-s) t (by simpa using hst)

Negation of First Vector Preserves Linear Independence of Pairs

Informal description

For any two vectors $x$ and $y$ in a module $M$ over a ring $R$, the family of vectors $[-x, y]$ is linearly independent if and only if the family $[x, y]$ is linearly independent.

LinearIndependent.pair_neg_right_iff theorem

: LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]

Full source

@[simp] lemma LinearIndependent.pair_neg_right_iff :
    LinearIndependentLinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y] := by
  rw [pair_symm_iff, pair_neg_left_iff, pair_symm_iff]

Negation of Second Vector Preserves Linear Independence of Pairs

Informal description

For any two vectors $x$ and $y$ in a module $M$ over a ring $R$, the family of vectors $[x, -y]$ is linearly independent if and only if the family $[x, y]$ is linearly independent.

LinearIndependent.pair_smul_iff theorem

{u : S} (hu : u ≠ 0) : LinearIndependent R ![u • x, u • y] ↔ LinearIndependent R ![x, y]

Full source

lemma LinearIndependent.pair_smul_iff {u : S} (hu : u ≠ 0) :
    LinearIndependentLinearIndependent R ![u • x, u • y] ↔ LinearIndependent R ![x, y] := by
  simp only [LinearIndependent.pair_iff]
  refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩
  · exact h s t (by rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero])
  · specialize h (u • s) (u • t) (by rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst])
    exact ⟨(smul_eq_zero_iff_right hu).mp h.1, (smul_eq_zero_iff_right hu).mp h.2⟩

Scalar Multiplication Preserves Linear Independence of Pairs

Informal description

Let $R$ be a ring, $S$ be a module over $R$, and $x, y$ be vectors in $S$. For any nonzero scalar $u \in S$, the pair of vectors $(u \cdot x, u \cdot y)$ is linearly independent over $R$ if and only if the pair $(x, y)$ is linearly independent over $R$.

LinearIndependent.pair_add_smul_add_smul_iff theorem

 [Nontrivial R] : LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Full source

@[simp] lemma LinearIndependent.pair_add_smul_add_smul_iff [Nontrivial R] :
    LinearIndependentLinearIndependent R ![a • x + b • y, c • x + d • y] ↔
      LinearIndependent R ![x, y] ∧ a * d ≠ b * c := by
  rcases eq_or_ne (a * d) (b * c) with h | h
  · suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [h]
    rw [pair_iff]
    push_neg
    by_cases hbd : b = 0 ∧ d = 0
    · simp only [hbd.1, hbd.2, zero_smul, add_zero]
      by_cases hac : a = 0 ∧ c = 0; · exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩
      refine ⟨c • 1, -a • 1, ?_, by aesop⟩
      simp only [smul_assoc, one_smul, neg_smul]
      module
    refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; aesop⟩
    simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]
    module
  refine ⟨fun h' ↦ ⟨?_, h⟩, fun ⟨h₁, h₂⟩ ↦ pair_add_smul_add_smul_iff_aux _ _ _ _ h₂ h₁⟩
  suffices LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y] by
    rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this
  convert pair_add_smul_add_smul_iff_aux d (-b) (-c) a (by simpa [mul_comm d a]) h' using 1
  ext i; fin_cases i <;> simp <;> module

Linear independence of transformed vector pairs: $(ax+by, cx+dy)$ independent iff $(x,y)$ independent and $ad \neq bc$

Informal description

Let $R$ be a nontrivial ring and $M$ an $R$-module. For any vectors $x, y \in M$ and scalars $a, b, c, d \in R$, the pair of vectors $(a \cdot x + b \cdot y, c \cdot x + d \cdot y)$ is linearly independent over $R$ if and only if the pair $(x, y)$ is linearly independent over $R$ and the determinant condition $a \cdot d \neq b \cdot c$ holds.

LinearIndependent.pair_add_smul_right_iff theorem

: LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Full source

@[simp] lemma LinearIndependent.pair_add_smul_right_iff :
    LinearIndependentLinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y] := by
  rcases subsingleton_or_nontrivial S with hS | hS; · simp [hS.elim c 0]
  nontriviality R
  simpa using pair_add_smul_add_smul_iff (x := x) (y := y) 1 0 c 1

Linear independence of $(x, cx + y)$ is equivalent to linear independence of $(x, y)$

Informal description

Let $R$ be a ring and $M$ an $R$-module. For any vectors $x, y \in M$ and scalar $c \in R$, the pair of vectors $(x, c \cdot x + y)$ is linearly independent over $R$ if and only if the pair $(x, y)$ is linearly independent over $R$.

LinearIndependent.pair_add_smul_left_iff theorem

: LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

Full source

@[simp] lemma LinearIndependent.pair_add_smul_left_iff :
    LinearIndependentLinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y] := by
  rcases subsingleton_or_nontrivial S with hS | hS; · simp [hS.elim b 0]
  nontriviality R
  simpa using pair_add_smul_add_smul_iff (x := x) (y := y) 1 b 0 1

Linear independence of $(x + b y, y)$ iff $(x, y)$ is linearly independent

Informal description

For any ring $R$ and $R$-module $M$, and for any vectors $x, y \in M$ and scalar $b \in R$, the pair of vectors $(x + b \cdot y, y)$ is linearly independent over $R$ if and only if the pair $(x, y)$ is linearly independent over $R$.

linearIndepOn_id_iUnion_finite theorem

 {f : ι → Set M} (hl : ∀ i, LinearIndepOn R id (f i))
  (hd : ∀ i, ∀ t : Set ι, t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))) :
  LinearIndepOn R id (⋃ i, f i)

Full source

theorem linearIndepOn_id_iUnion_finite {f : ι → Set M} (hl : ∀ i, LinearIndepOn R id (f i))
    (hd : ∀ i, ∀ t : Set ι, t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))) :
    LinearIndepOn R id (⋃ i, f i) := by
  classical
  rw [iUnion_eq_iUnion_finset f]
  apply linearIndepOn_iUnion_of_directed
  · apply directed_of_isDirected_le
    exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h
  intro t
  induction t using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his

Linear Independence Preserved Under Union of Disjointly Spanning Subsets

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $\{f_i\}_{i \in \iota}$ a family of subsets of $M$ indexed by $\iota$. Suppose that: 1. For each $i \in \iota$, the vectors in $f_i$ are linearly independent over $R$ (when considered as a family via the identity map). 2. For each $i \in \iota$ and any finite subset $t \subseteq \iota$ not containing $i$, the span of $f_i$ is disjoint from the span of $\bigcup_{j \in t} f_j$, i.e., \[ \text{span}_R(f_i) \cap \left( \bigsqcup_{j \in t} \text{span}_R(f_j) \right) = \{0\}. \] Then the vectors in $\bigcup_{i \in \iota} f_i$ are linearly independent over $R$ (when considered as a family via the identity map).

linearIndependent_iUnion_finite theorem

 {η : Type*} {ιs : η → Type*} {f : ∀ j : η, ιs j → M} (hindep : ∀ j, LinearIndependent R (f j))
  (hd : ∀ i, ∀ t : Set η, t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))) :
  LinearIndependent R fun ji : Σ j, ιs j => f ji.1 ji.2

Full source

theorem linearIndependent_iUnion_finite {η : Type*} {ιs : η → Type*} {f : ∀ j : η, ιs j → M}
    (hindep : ∀ j, LinearIndependent R (f j))
    (hd : ∀ i, ∀ t : Set η,
      t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))) :
    LinearIndependent R fun ji : Σ j, ιs j => f ji.1 ji.2 := by
  nontriviality R
  apply LinearIndependent.of_linearIndepOn_id_range
  · rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy
    by_cases h_cases : x₁ = y₁
    · subst h_cases
      refine Sigma.eq rfl ?_
      rw [LinearIndependent.injective (hindep _) hxy]
    · have h0 : f x₁ x₂ = 0 := by
        apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))
        rw [iSup_singleton]
        simp only at hxy
        rw [hxy]
        exact subset_span (mem_range_self y₂)
      exact False.elim ((hindep x₁).ne_zero _ h0)
  rw [range_sigma_eq_iUnion_range]
  apply linearIndepOn_id_iUnion_finite (fun j => (hindep j).linearIndepOn_id) hd

Linear Independence of Union of Disjointly Spanning Families

Informal description

Let $R$ be a ring, $M$ an $R$-module, $\eta$ a type, and $\{\iota_j\}_{j \in \eta}$ a family of types indexed by $\eta$. For each $j \in \eta$, let $f_j : \iota_j \to M$ be a family of vectors in $M$. Suppose that: 1. For each $j \in \eta$, the family $f_j$ is linearly independent over $R$. 2. For each $i \in \eta$ and any finite subset $t \subseteq \eta$ not containing $i$, the span of the range of $f_i$ is disjoint from the span of the union of the ranges of $\{f_j\}_{j \in t}$, i.e., \[ \text{span}_R(\text{range } f_i) \cap \left( \bigsqcup_{j \in t} \text{span}_R(\text{range } f_j) \right) = \{0\}. \] Then the combined family $(j, k) \mapsto f_j(k)$ (where $(j, k) \in \Sigma_{j \in \eta} \iota_j$) is linearly independent over $R$.

exists_maximal_linearIndepOn theorem

 (v : ι → M) : ∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ i ∉ s, ∃ a : R, a ≠ 0 ∧ a • v i ∈ span R (v '' s)

Full source

theorem exists_maximal_linearIndepOn (v : ι → M) :
    ∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ i ∉ s, ∃ a : R, a ≠ 0 ∧ a • v i ∈ span R (v '' s) := by
  classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ Jx ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact hIlinind (Finsupp.mem_support_iff.mp hx)
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.not_mem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)

Existence of Maximal Linearly Independent Subset with Spanning Property

Informal description

For any family of vectors $v \colon \iota \to M$ in a module $M$ over a ring $R$, there exists a subset $s \subseteq \iota$ such that: 1. The family $\{v_i\}_{i \in s}$ is linearly independent over $R$. 2. For any index $i \notin s$, there exists a nonzero scalar $a \in R$ such that the vector $a \cdot v_i$ lies in the span of $\{v_j\}_{j \in s}$.

LinearIndependent.restrict_scalars' theorem

 (R : Type*) {S M ι : Type*} [CommSemiring R] [Semiring S] [Algebra R S] [FaithfulSMul R S] [AddCommMonoid M]
  [Module R M] [Module S M] [IsScalarTower R S M] {v : ι → M} (li : LinearIndependent S v) : LinearIndependent R v

Full source

theorem LinearIndependent.restrict_scalars' (R : Type*) {S M ι : Type*}
    [CommSemiring R] [Semiring S] [Algebra R S] [FaithfulSMul R S]
    [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M]
    {v : ι → M} (li : LinearIndependent S v) :
    LinearIndependent R v :=
  restrict_scalars ((faithfulSMul_iff_injective_smul_one R S).mp inferInstance) li

Linear Independence Preserved Under Faithful Restriction of Scalars

Informal description

Let $R$ be a commutative semiring and $S$ a semiring with an algebra structure over $R$ such that the scalar multiplication action of $R$ on $S$ is faithful. Let $M$ be an $R$-module and an $S$-module with compatible scalar multiplication (i.e., $r \cdot (s \cdot m) = (r \cdot s) \cdot m$ for all $r \in R$, $s \in S$, $m \in M$). If a family of vectors $\{v_i\}_{i \in \iota}$ in $M$ is linearly independent over $S$, then it is also linearly independent over $R$.

linearIndependent_algHom_toLinearMap theorem

 (K M L) [CommSemiring K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] :
  LinearIndependent L (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L)

Full source

@[stacks 0CKM]
lemma linearIndependent_algHom_toLinearMap
    (K M L) [CommSemiring K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] :
    LinearIndependent L (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L) := by
  apply LinearIndependent.of_comp (LinearMap.ltoFun K M L)
  exact (linearIndependent_monoidHom M L).comp
    (RingHom.toMonoidHomRingHom.toMonoidHom ∘ AlgHom.toRingHom)
    (fun _ _ e ↦ AlgHom.ext (DFunLike.congr_fun e :))

Linear Independence of Algebra Homomorphisms as Linear Maps over $L$ (Generalized Dedekind's Theorem)

Informal description

Let $K$ be a commutative semiring, $M$ a semiring with an algebra structure over $K$, and $L$ a commutative domain with an algebra structure over $K$. Then the set of algebra homomorphisms from $M$ to $L$, considered as linear maps via the canonical embedding $\text{AlgHom.toLinearMap} \colon (M \to_{K\text{-alg}} L) \to (M \to_{K\text{-lin}} L)$, is linearly independent over $L$.

linearIndependent_algHom_toLinearMap' theorem

 (K M L) [CommRing K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] [NoZeroSMulDivisors K L] :
  LinearIndependent K (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L)

Full source

lemma linearIndependent_algHom_toLinearMap' (K M L) [CommRing K]
    [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] [NoZeroSMulDivisors K L] :
    LinearIndependent K (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L) :=
  (linearIndependent_algHom_toLinearMap K M L).restrict_scalars' K

Linear Independence of Algebra Homomorphisms over $K$ (Generalized Dedekind's Theorem)

Informal description

Let $K$ be a commutative ring, $M$ a semiring with an algebra structure over $K$, and $L$ a commutative domain with an algebra structure over $K$ such that $K$ and $L$ have no zero scalar multiplication divisors. Then the set of algebra homomorphisms from $M$ to $L$, considered as linear maps via the canonical embedding $\text{AlgHom.toLinearMap} \colon (M \to_{K\text{-alg}} L) \to (M \to_{K\text{-lin}} L)$, is linearly independent over $K$.

mem_span_insert_exchange theorem

: x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s)

Full source

theorem mem_span_insert_exchange :
    x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s) := by
  simp only [mem_span_insert, forall_exists_index, and_imp]
  rintro a z hz rfl h
  refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩
  have a0 : a ≠ 0 := by
    rintro rfl
    simp_all
  match_scalars <;> simp [a0]

Exchange Lemma for Linear Spans: $x \in \text{span}(s \cup \{y\}) \setminus \text{span}(s) \implies y \in \text{span}(s \cup \{x\})$

Informal description

Let $K$ be a division ring, $V$ a module over $K$, and $s$ a set of vectors in $V$. For any vectors $x, y \in V$, if $x$ is in the span of $s \cup \{y\}$ but not in the span of $s$, then $y$ is in the span of $s \cup \{x\}$.

LinearIndepOn.insert theorem

(hs : LinearIndepOn K id s) (hx : x ∉ span K s) : LinearIndepOn K id (insert x s)

Full source

protected theorem LinearIndepOn.insert (hs : LinearIndepOn K id s) (hx : x ∉ span K s) :
    LinearIndepOn K id (insert x s) := by
  rw [← union_singleton]
  have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem (span K s)) hx
  apply hs.id_union (LinearIndepOn.id_singleton _ x0)
  rwa [disjoint_span_singleton' x0]

Linear Independence Preserved Under Insertion of Vector Outside Span

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $s \subseteq V$ a set of vectors. If: 1. The vectors in $s$ are linearly independent over $K$ (when considered as a family via the identity map), and 2. The vector $x \in V$ does not lie in the span of $s$, then the set $\{x\} \cup s$ is linearly independent over $K$ (when considered as a family via the identity map).

linearIndependent_option' theorem

 :
  LinearIndependent K (fun o => Option.casesOn' o x v : Option ι → V) ↔
    LinearIndependent K v ∧ x ∉ Submodule.span K (range v)

Full source

theorem linearIndependent_option' :
    LinearIndependentLinearIndependent K (fun o => Option.casesOn' o x v : Option ι → V) ↔
      LinearIndependent K v ∧ x ∉ Submodule.span K (range v) := by
  -- Porting note: Explicit universe level is required in `Equiv.optionEquivSumPUnit`.
  rw [← linearIndependent_equiv (Equiv.optionEquivSumPUnit.{u', _} ι).symm, linearIndependent_sum,
    @range_unique _ PUnit, @linearIndependent_unique_iff PUnit, disjoint_span_singleton]
  dsimp [(· ∘ ·)]
  refine ⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, ?_, fun hx => (h.2 hx).elim⟩⟩
  rintro rfl
  exact h.2 (zero_mem _)

Linear Independence Criterion for Option-Extended Family: $f$ is linearly independent iff $v$ is linearly independent and $x \notin \text{span}(\text{range}(v))$

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $v : \iota \to V$ a family of vectors, and $x \in V$. The family of vectors defined by $f(o) = \begin{cases} x & \text{if } o = \text{none} \\ v(i) & \text{if } o = \text{some } i \end{cases}$ is linearly independent over $K$ if and only if: 1. The family $v$ is linearly independent over $K$, and 2. The vector $x$ does not lie in the span of the range of $v$.

LinearIndependent.option theorem

 (hv : LinearIndependent K v) (hx : x ∉ Submodule.span K (range v)) :
  LinearIndependent K (fun o => Option.casesOn' o x v : Option ι → V)

Full source

theorem LinearIndependent.option (hv : LinearIndependent K v)
    (hx : x ∉ Submodule.span K (range v)) :
    LinearIndependent K (fun o => Option.casesOn' o x v : Option ι → V) :=
  linearIndependent_option'.2 ⟨hv, hx⟩

Linear Independence of Option-Extended Family

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $v : \iota \to V$ a linearly independent family of vectors, and $x \in V$ a vector not in the span of the range of $v$. Then the extended family of vectors $f : \text{Option } \iota \to V$ defined by $$ f(o) = \begin{cases} x & \text{if } o = \text{none} \\ v(i) & \text{if } o = \text{some } i \end{cases} $$ is linearly independent over $K$.

linearIndependent_option theorem

 {v : Option ι → V} :
  LinearIndependent K v ↔ LinearIndependent K (v ∘ (↑) : ι → V) ∧ v none ∉ Submodule.span K (range (v ∘ (↑) : ι → V))

Full source

theorem linearIndependent_option {v : Option ι → V} : LinearIndependentLinearIndependent K v ↔
    LinearIndependent K (v ∘ (↑) : ι → V) ∧
      v none ∉ Submodule.span K (range (v ∘ (↑) : ι → V)) := by
  simp only [← linearIndependent_option', Option.casesOn'_none_coe]

Linear Independence Criterion for Option-Indexed Vectors

Informal description

A family of vectors $v : \text{Option } \iota \to V$ is linearly independent over a field $K$ if and only if: 1. The restriction of $v$ to $\iota$ (via the coercion $\iota \hookrightarrow \text{Option } \iota$) is linearly independent, and 2. The vector $v(\text{none})$ does not lie in the span of the range of $v$ restricted to $\iota$.

linearIndepOn_insert theorem

 {s : Set ι} {a : ι} {f : ι → V} (has : a ∉ s) :
  LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s)

Full source

theorem linearIndepOn_insert {s : Set ι} {a : ι} {f : ι → V} (has : a ∉ s) :
    LinearIndepOnLinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s) := by
  classical
  rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
    ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]
  simp only [comp_def]
  rw [range_comp']
  simp

Linear Independence Criterion for Insertion: $f$ is linearly independent on $\{a\} \cup s$ iff $f$ is independent on $s$ and $f(a) \notin \text{span}_K(f(s))$

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $s$ a subset of $\iota$, $a \in \iota$ with $a \notin s$, and $f : \iota \to V$ a family of vectors. The family $f$ is linearly independent on the set $\{a\} \cup s$ if and only if: 1. $f$ is linearly independent on $s$, and 2. The vector $f(a)$ does not lie in the span of the image of $s$ under $f$.

linearIndepOn_id_insert theorem

(hxs : x ∉ s) : LinearIndepOn K id (insert x s) ↔ LinearIndepOn K id s ∧ x ∉ Submodule.span K s

Full source

theorem linearIndepOn_id_insert (hxs : x ∉ s) :
    LinearIndepOnLinearIndepOn K id (insert x s) ↔ LinearIndepOn K id s ∧ x ∉ Submodule.span K s :=
  (linearIndepOn_insert (f := id) hxs).trans <| by simp

Linear Independence Criterion for Insertion of Identity: $\{x\} \cup s$ is linearly independent iff $s$ is independent and $x \notin \text{span}_K(s)$

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $s$ a subset of $V$, and $x \in V$ with $x \notin s$. The set $\{x\} \cup s$ is linearly independent over $K$ if and only if: 1. $s$ is linearly independent over $K$, and 2. $x$ does not lie in the span of $s$ over $K$.

linearIndepOn_insert_iff theorem

 {s : Set ι} {a : ι} {f : ι → V} :
  LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s)

Full source

theorem linearIndepOn_insert_iff {s : Set ι} {a : ι} {f : ι → V} :
    LinearIndepOnLinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s) := by
  by_cases has : a ∈ s
  · simp [insert_eq_of_mem has, has]
  simp [linearIndepOn_insert has, has]

Linear Independence Criterion for Insertion: $f$ is linearly independent on $\{a\} \cup s$ iff $f$ is independent on $s$ and $f(a) \in \text{span}_K(f(s)) \Rightarrow a \in s$

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $s \subseteq \iota$ a subset, $a \in \iota$, and $f : \iota \to V$ a family of vectors. The family $f$ is linearly independent on the set $\{a\} \cup s$ if and only if: 1. $f$ is linearly independent on $s$, and 2. For any vector $f(a)$ in the span of $f(s)$, it must be that $a \in s$.

linearIndepOn_id_insert_iff theorem

{a : V} {s : Set V} : LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ span K s → a ∈ s)

Full source

theorem linearIndepOn_id_insert_iff {a : V} {s : Set V} :
    LinearIndepOnLinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ span K s → a ∈ s) := by
  simpa using linearIndepOn_insert_iff (a := a) (f := id)

Linear Independence Criterion for Insertion of Identity: $\{a\} \cup s$ is independent iff $s$ is independent and $a \in \text{span}_K(s) \Rightarrow a \in s$

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $s$ a subset of $V$, and $a \in V$. The set $\{a\} \cup s$ is linearly independent over $K$ if and only if: 1. $s$ is linearly independent over $K$, and 2. If $a$ lies in the span of $s$ over $K$, then $a$ must already be an element of $s$.

LinearIndepOn.mem_span_iff theorem

 {s : Set ι} {a : ι} {f : ι → V} (h : LinearIndepOn K f s) :
  f a ∈ Submodule.span K (f '' s) ↔ (LinearIndepOn K f (insert a s) → a ∈ s)

Full source

theorem LinearIndepOn.mem_span_iff {s : Set ι} {a : ι} {f : ι → V} (h : LinearIndepOn K f s) :
    f a ∈ Submodule.span K (f '' s)f a ∈ Submodule.span K (f '' s) ↔ (LinearIndepOn K f (insert a s) → a ∈ s) := by
  by_cases has : a ∈ s
  · exact iff_of_true (subset_span <| mem_image_of_mem f has) fun _ ↦ has
  simp [linearIndepOn_insert_iff, h, has]

Span Membership Criterion for Linear Independence

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $\iota$ an index set, $f : \iota \to V$ a family of vectors, and $s \subseteq \iota$ a subset such that $\{f_i\}_{i \in s}$ is linearly independent over $K$. For any $a \in \iota$, the following equivalence holds: $f_a$ belongs to the span of $\{f_i\}_{i \in s}$ if and only if, whenever $\{f_i\}_{i \in s \cup \{a\}}$ is linearly independent, it must be that $a \in s$.

LinearIndepOn.not_mem_span_iff theorem

 {s : Set ι} {a : ι} {f : ι → V} (h : LinearIndepOn K f s) :
  f a ∉ Submodule.span K (f '' s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s

Full source

/-- A shortcut to a convenient form for the negation in `LinearIndepOn.mem_span_iff`. -/
theorem LinearIndepOn.not_mem_span_iff {s : Set ι} {a : ι} {f : ι → V} (h : LinearIndepOn K f s) :
    f a ∉ Submodule.span K (f '' s)f a ∉ Submodule.span K (f '' s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s := by
  rw [h.mem_span_iff, _root_.not_imp]

Non-membership in Span Criterion for Linear Independence

Informal description

Let $K$ be a division ring, $V$ a $K$-module, $\iota$ an index set, $f : \iota \to V$ a family of vectors, and $s \subseteq \iota$ a subset such that $\{f_i\}_{i \in s}$ is linearly independent over $K$. For any $a \in \iota$, the following equivalence holds: $f_a$ does not belong to the span of $\{f_i\}_{i \in s}$ if and only if $\{f_i\}_{i \in s \cup \{a\}}$ is linearly independent and $a \notin s$.

LinearIndepOn.mem_span_iff_id theorem

 {s : Set V} {a : V} (h : LinearIndepOn K id s) : a ∈ Submodule.span K s ↔ (LinearIndepOn K id (insert a s) → a ∈ s)

Full source

theorem LinearIndepOn.mem_span_iff_id {s : Set V} {a : V} (h : LinearIndepOn K id s) :
    a ∈ Submodule.span K sa ∈ Submodule.span K s ↔ (LinearIndepOn K id (insert a s) → a ∈ s) := by
  simpa using h.mem_span_iff (a := a)

Span Membership Criterion for Linear Independence (Identity Version)

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $s \subseteq V$ a linearly independent subset. For any vector $a \in V$, the following equivalence holds: $a$ belongs to the span of $s$ if and only if, whenever $s \cup \{a\}$ is linearly independent, it must be that $a \in s$.

LinearIndepOn.not_mem_span_iff_id theorem

 {s : Set V} {a : V} (h : LinearIndepOn K id s) : a ∉ Submodule.span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s

Full source

theorem LinearIndepOn.not_mem_span_iff_id {s : Set V} {a : V} (h : LinearIndepOn K id s) :
    a ∉ Submodule.span K sa ∉ Submodule.span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s := by
  rw [h.mem_span_iff_id, _root_.not_imp]

Non-membership in Span Criterion for Linear Independence (Identity Version)

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $s \subseteq V$ a linearly independent subset. For any vector $a \in V$, the following equivalence holds: $a$ does not belong to the span of $s$ if and only if the set $s \cup \{a\}$ is linearly independent and $a \notin s$.

linearIndepOn_id_pair theorem

{x y : V} (hx : x ≠ 0) (hy : ∀ a : K, a • x ≠ y) : LinearIndepOn K id { x, y }

Full source

theorem linearIndepOn_id_pair {x y : V} (hx : x ≠ 0) (hy : ∀ a : K, a • x ≠ y) :
    LinearIndepOn K id {x, y} :=
  pair_comm y x ▸ (LinearIndepOn.id_singleton K hx).insert (x := y) <|
    mt mem_span_singleton.1 <| not_exists.2 hy

Linear Independence Criterion for Vector Pairs: $\{x, y\}$ independent iff $y \notin K \cdot x$

Informal description

Let $K$ be a division ring and $V$ a $K$-module. For any two vectors $x, y \in V$ such that: 1. $x \neq 0$, and 2. $y$ is not a scalar multiple of $x$ (i.e., there exists no $a \in K$ such that $y = a \cdot x$), the set $\{x, y\}$ is linearly independent over $K$ when considered as a family via the identity map.

linearIndepOn_pair_iff theorem

 {i j : ι} (v : ι → V) (hij : i ≠ j) (hi : v i ≠ 0) : LinearIndepOn K v { i, j } ↔ ∀ (c : K), c • v i ≠ v j

Full source

/-- `LinearIndepOn.pair_iff` is a version that works over arbitrary rings. -/
theorem linearIndepOn_pair_iff {i j : ι} (v : ι → V) (hij : i ≠ j) (hi : v i ≠ 0):
    LinearIndepOnLinearIndepOn K v {i, j} ↔ ∀ (c : K), c • v i ≠ v j := by
  rw [pair_comm]
  convert linearIndepOn_insert (s := {i}) (a := j) hij.symm
  simp [hi, mem_span_singleton, linearIndependent_unique_iff]

Linear Independence Criterion for Vector Pairs: $\{v_i, v_j\}$ independent iff $v_j \notin K \cdot v_i$

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $v : \iota \to V$ a family of vectors. For any two distinct indices $i,j \in \iota$ with $v_i \neq 0$, the vectors $\{v_i, v_j\}$ are linearly independent over $K$ if and only if there exists no scalar $c \in K$ such that $v_j = c \cdot v_i$.

LinearIndependent.pair_iff' theorem

{x y : V} (hx : x ≠ 0) : LinearIndependent K ![x, y] ↔ ∀ a : K, a • x ≠ y

Full source

/-- Also see `LinearIndependent.pair_iff` for the version over arbitrary rings. -/
theorem LinearIndependent.pair_iff' {x y : V} (hx : x ≠ 0) :
    LinearIndependentLinearIndependent K ![x, y] ↔ ∀ a : K, a • x ≠ y := by
  rw [← linearIndepOn_univ, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0,1} from rfl,
    Finset.coe_insert, Finset.coe_singleton, linearIndepOn_pair_iff _ (by simp) (by simpa)]
  simp

Linear Independence Criterion for Vector Pairs: $[x, y]$ independent iff $y \notin K \cdot x$

Informal description

Let $K$ be a division ring and $V$ a $K$-module. For any two vectors $x, y \in V$ with $x \neq 0$, the family of vectors $[x, y]$ is linearly independent over $K$ if and only if there exists no scalar $a \in K$ such that $y = a \cdot x$.

linearIndependent_fin_cons theorem

 {n} {v : Fin n → V} :
  LinearIndependent K (Fin.cons x v : Fin (n + 1) → V) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (range v)

Full source

theorem linearIndependent_fin_cons {n} {v : Fin n → V} :
    LinearIndependentLinearIndependent K (Fin.cons x v : Fin (n + 1) → V) ↔
      LinearIndependent K v ∧ x ∉ Submodule.span K (range v) := by
  rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]
  exact Iff.rfl

Linear Independence Criterion for Prepended Vector Family: $\text{Fin.cons}(x, v)$ is linearly independent iff $v$ is linearly independent and $x \notin \text{span}(v)$

Informal description

Let $K$ be a field, $V$ a $K$-vector space, and $n$ a natural number. For a vector $x \in V$ and a family of vectors $v : \text{Fin}(n) \to V$, the extended family $\text{Fin.cons}(x, v) : \text{Fin}(n+1) \to V$ is linearly independent over $K$ if and only if: 1. The family $v$ is linearly independent over $K$, and 2. The vector $x$ does not lie in the span of the range of $v$. Here, $\text{Fin.cons}(x, v)$ denotes the family obtained by prepending $x$ to $v$, i.e., it maps $0$ to $x$ and $i+1$ to $v(i)$ for $i \in \text{Fin}(n)$.

linearIndependent_fin_snoc theorem

 {n} {v : Fin n → V} :
  LinearIndependent K (Fin.snoc v x : Fin (n + 1) → V) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (range v)

Full source

theorem linearIndependent_fin_snoc {n} {v : Fin n → V} :
    LinearIndependentLinearIndependent K (Fin.snoc v x : Fin (n + 1) → V) ↔
      LinearIndependent K v ∧ x ∉ Submodule.span K (range v) := by
  rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv,
    linearIndependent_fin_cons]

Linear Independence Criterion for Appended Vector Family: $\text{Fin.snoc}(v, x)$ is linearly independent iff $v$ is linearly independent and $x \notin \text{span}(v)$

Informal description

Let $K$ be a field, $V$ a $K$-vector space, and $n$ a natural number. For a vector $x \in V$ and a family of vectors $v : \text{Fin}(n) \to V$, the extended family $\text{Fin.snoc}(v, x) : \text{Fin}(n+1) \to V$ is linearly independent over $K$ if and only if: 1. The family $v$ is linearly independent over $K$, and 2. The vector $x$ does not lie in the span of the range of $v$. Here, $\text{Fin.snoc}(v, x)$ denotes the family obtained by appending $x$ to $v$, i.e., it maps $i$ to $v(i)$ for $i \in \text{Fin}(n)$ and the last index to $x$.

LinearIndependent.fin_cons theorem

 {n} {v : Fin n → V} (hv : LinearIndependent K v) (hx : x ∉ Submodule.span K (range v)) :
  LinearIndependent K (Fin.cons x v : Fin (n + 1) → V)

Full source

/-- See `LinearIndependent.fin_cons'` for an uglier version that works if you
only have a module over a semiring. -/
theorem LinearIndependent.fin_cons {n} {v : Fin n → V} (hv : LinearIndependent K v)
    (hx : x ∉ Submodule.span K (range v)) : LinearIndependent K (Fin.cons x v : Fin (n + 1) → V) :=
  linearIndependent_fin_cons.2 ⟨hv, hx⟩

Linear Independence of Prepended Vector Family

Informal description

Let $K$ be a field, $V$ a $K$-vector space, and $n$ a natural number. Given a linearly independent family of vectors $v : \text{Fin}(n) \to V$ and a vector $x \in V$ not in the span of $v$, then the extended family $\text{Fin.cons}(x, v) : \text{Fin}(n+1) \to V$ is also linearly independent over $K$. Here, $\text{Fin.cons}(x, v)$ denotes the family obtained by prepending $x$ to $v$, i.e., it maps $0$ to $x$ and $i+1$ to $v(i)$ for $i \in \text{Fin}(n)$.

linearIndependent_fin_succ theorem

 {n} {v : Fin (n + 1) → V} :
  LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (range <| Fin.tail v)

Full source

theorem linearIndependent_fin_succ {n} {v : Fin (n + 1) → V} :
    LinearIndependentLinearIndependent K v ↔
      LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (range <| Fin.tail v) := by
  rw [← linearIndependent_fin_cons, Fin.cons_self_tail]

Linear Independence Criterion for Finite Families: $v$ is linearly independent iff its tail is linearly independent and $v(0) \notin \text{span}(\text{tail}(v))$

Informal description

For any natural number $n$ and any family of vectors $v : \text{Fin}(n+1) \to V$ in a vector space $V$ over a field $K$, the family $v$ is linearly independent if and only if: 1. The tail of $v$ (i.e., the family obtained by removing the first vector) is linearly independent, and 2. The first vector $v(0)$ does not lie in the span of the range of the tail of $v$. Here, $\text{Fin}(n+1)$ denotes the finite type with $n+1$ elements, and $\text{Fin.tail}(v)$ is the family $v$ restricted to indices $1$ through $n$.

linearIndependent_fin_succ' theorem

 {n} {v : Fin (n + 1) → V} :
  LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last _) ∉ Submodule.span K (range <| Fin.init v)

Full source

theorem linearIndependent_fin_succ' {n} {v : Fin (n + 1) → V} : LinearIndependentLinearIndependent K v ↔
    LinearIndependent K (Fin.init v) ∧ v (Fin.last _) ∉ Submodule.span K (range <| Fin.init v) := by
  rw [← linearIndependent_fin_snoc, Fin.snoc_init_self]

Linear Independence Criterion for Finite Families: $v$ is linearly independent iff its initial segment is linearly independent and $v(\text{last } n) \notin \text{span}(\text{init}(v))$

Informal description

For any natural number $n$ and any family of vectors $v : \text{Fin}(n+1) \to V$ in a vector space $V$ over a field $K$, the family $v$ is linearly independent if and only if: 1. The initial segment $\text{Fin.init}(v) : \text{Fin}(n) \to V$ is linearly independent, and 2. The last vector $v(\text{last } n)$ does not lie in the span of the range of $\text{Fin.init}(v)$. Here, $\text{Fin.init}(v)$ denotes the family obtained by removing the last vector from $v$, and $\text{last } n$ is the index of the last element in $\text{Fin}(n+1)$.

equiv_linearIndependent definition

 (n : ℕ) :
  { s : Fin (n + 1) → V // LinearIndependent K s } ≃
    Σ s : { s : Fin n → V // LinearIndependent K s }, ((Submodule.span K (Set.range (s : Fin n → V)))ᶜ : Set V)

Full source

/-- Equivalence between `k + 1` vectors of length `n` and `k` vectors of length `n` along with a
vector in the complement of their span.
-/
def equiv_linearIndependent (n : ℕ) :
    { s : Fin (n + 1) → V // LinearIndependent K s }{ s : Fin (n + 1) → V // LinearIndependent K s } ≃
      Σ s : { s : Fin n → V // LinearIndependent K s },
        ((Submodule.span K (Set.range (s : Fin n → V)))ᶜ : Set V) where
  toFun s := ⟨⟨Fin.tail s.val, (linearIndependent_fin_succ.mp s.property).left⟩,
    ⟨s.val 0, (linearIndependent_fin_succ.mp s.property).right⟩⟩
  invFun s := ⟨Fin.cons s.2.val s.1.val,
    linearIndependent_fin_cons.mpr ⟨s.1.property, s.2.property⟩⟩
  left_inv _ := by simp only [Fin.cons_self_tail, Subtype.coe_eta]
  right_inv := fun ⟨_, _⟩ => by simp only [Fin.cons_zero, Subtype.coe_eta, Sigma.mk.inj_iff,
    Fin.tail_cons, heq_eq_eq, and_self]

Bijection between linearly independent families of $ n+1 $ vectors and pairs of linearly independent families of $ n $ vectors with a vector outside their span

Informal description

For any natural number $ n $, there is a bijection between: 1. The set of linearly independent families of $ n+1 $ vectors in a vector space $ V $ over a field $ K $, and 2. The set of pairs consisting of: - A linearly independent family of $ n $ vectors in $ V $, and - A vector in the complement of the span of these $ n $ vectors. The bijection is given by: - The forward direction maps a family $ s $ of $ n+1 $ vectors to the pair $ (\text{tail}(s), s(0)) $, where $ \text{tail}(s) $ is the family obtained by removing the first vector, and $ s(0) $ is the first vector (which must lie outside the span of the tail). - The backward direction maps a pair $ (s, v) $ to the family obtained by prepending $ v $ to $ s $, which is linearly independent if and only if $ v $ is not in the span of $ s $.

linearIndependent_fin2 theorem

{f : Fin 2 → V} : LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ a : K, a • f 1 ≠ f 0

Full source

theorem linearIndependent_fin2 {f : Fin 2 → V} :
    LinearIndependentLinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ a : K, a • f 1 ≠ f 0 := by
  rw [linearIndependent_fin_succ, linearIndependent_unique_iff, range_unique, mem_span_singleton,
    not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]

Linear Independence Criterion for Pairs of Vectors: $f$ is linearly independent iff $f(1) \neq 0$ and $f(0)$ is not a scalar multiple of $f(1)$

Informal description

For any family of vectors $f \colon \text{Fin}(2) \to V$ in a vector space $V$ over a field $K$, the family $f$ is linearly independent if and only if: 1. The vector $f(1)$ is nonzero, and 2. For every scalar $a \in K$, the vector $a \cdot f(1)$ is not equal to $f(0)$. Here, $\text{Fin}(2)$ denotes the finite type with two elements (indices 0 and 1).

exists_linearIndepOn_id_extension theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) : ∃ b ⊆ t, s ⊆ b ∧ t ⊆ span K b ∧ LinearIndepOn K id b

Full source

/-- TODO : generalize this and related results to non-identity functions -/
theorem exists_linearIndepOn_id_extension (hs : LinearIndepOn K id s) (hst : s ⊆ t) :
    ∃ b ⊆ t, s ⊆ b ∧ t ⊆ span K b ∧ LinearIndepOn K id b := by
  obtain ⟨b, sb, h⟩ := by
    refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K id b} ?_ _ ⟨hst, hs⟩
    · refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
      · exact sUnion_subset fun x xc => (hc xc).1
      · exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2
      · exact subset_sUnion_of_mem
  refine ⟨b, h.prop.1, sb, fun x xt => by_contra fun hn ↦ hn ?_, h.prop.2⟩
  exact subset_span <| h.mem_of_prop_insert ⟨insert_subset xt h.prop.1, h.prop.2.insert hn⟩

Extension of Linearly Independent Set to Basis Within Larger Set

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $s, t \subseteq V$ sets of vectors such that $s \subseteq t$. If the vectors in $s$ are linearly independent over $K$ (when considered as a family via the identity map), then there exists a subset $b \subseteq t$ such that: 1. $s \subseteq b$, 2. $t$ is contained in the span of $b$ over $K$, and 3. The vectors in $b$ are linearly independent over $K$ (when considered as a family via the identity map).

exists_linearIndependent theorem

: ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K ((↑) : b → V)

Full source

theorem exists_linearIndependent :
    ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K ((↑) : b → V) := by
  obtain ⟨b, hb₁, -, hb₂, hb₃⟩ :=
    exists_linearIndepOn_id_extension (linearIndependent_empty K V) (Set.empty_subset t)
  exact ⟨b, hb₁, (span_eq_of_le _ hb₂ (Submodule.span_mono hb₁)).symm, hb₃⟩

Existence of Linearly Independent Spanning Subset in Vector Spaces over Division Rings

Informal description

Let $K$ be a division ring and $V$ a $K$-module. For any subset $t \subseteq V$, there exists a subset $b \subseteq t$ such that: 1. The span of $b$ over $K$ equals the span of $t$ over $K$, i.e., $\text{span}_K b = \text{span}_K t$, and 2. The vectors in $b$ are linearly independent over $K$ (when considered as a family via the inclusion map $b \hookrightarrow V$).

exists_linearIndependent' theorem

 (v : ι → V) :
  ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧ LinearIndependent K (v ∘ a)

Full source

/-- Indexed version of `exists_linearIndependent`. -/
lemma exists_linearIndependent' (v : ι → V) :
    ∃ (κ : Type u') (a : κ → ι), Injective a ∧
      Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧
      LinearIndependent K (v ∘ a) := by
  obtain ⟨t, ht, hsp, hli⟩ := exists_linearIndependent K (Set.range v)
  choose f hf using ht
  let s : Set ι := Set.range (fun a : t ↦ f a.property)
  have hs {i : ι} (hi : i ∈ s) : v i ∈ t := by obtain ⟨a, rfl⟩ := hi; simp [hf]
  let f' (a : s) : t := ⟨v a.val, hs a.property⟩
  refine ⟨s, Subtype.val, Subtype.val_injective, hsp.symm ▸ by congr; aesop, ?_⟩
  · rw [← show Subtype.valSubtype.val ∘ f' = v ∘ Subtype.val by ext; simp [f']]
    apply hli.comp
    rintro ⟨i, x, rfl⟩ ⟨j, y, rfl⟩ hij
    simp only [Subtype.ext_iff, hf, f'] at hij
    simp [hij]

Existence of Linearly Independent Spanning Subfamily via Injective Restriction

Informal description

Let $K$ be a division ring and $V$ a $K$-module. For any family of vectors $v : \iota \to V$, there exists a type $\kappa$ and an injective function $a : \kappa \to \iota$ such that: 1. The span of the subfamily $v \circ a$ equals the span of the original family $v$, i.e., $\text{span}_K (\text{range}(v \circ a)) = \text{span}_K (\text{range}(v))$, and 2. The subfamily $v \circ a$ is linearly independent over $K$.

LinearIndepOn.extend definition

(hs : LinearIndepOn K id s) (hst : s ⊆ t) : Set V

Full source

/-- `LinearIndepOn.extend` adds vectors to a linear independent set `s ⊆ t` until it spans
all elements of `t`.
TODO - generalize the lemmas below to functions that aren't the identity. -/
noncomputable def LinearIndepOn.extend (hs : LinearIndepOn K id s) (hst : s ⊆ t) : Set V :=
  Classical.choose (exists_linearIndepOn_id_extension hs hst)

Maximal linearly independent extension of a subset

Informal description

Given a division ring $ K $, a $ K $-module $ V $, and subsets $ s \subseteq t \subseteq V $, if the vectors in $ s $ are linearly independent over $ K $ (when considered as a family via the identity map), then `LinearIndepOn.extend hs hst` is a subset of $ t $ containing $ s $ that is linearly independent and spans $ t $. Specifically, it is a maximal linearly independent subset of $ t $ extending $ s $.

LinearIndepOn.extend_subset theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) : hs.extend hst ⊆ t

Full source

theorem LinearIndepOn.extend_subset (hs : LinearIndepOn K id s) (hst : s ⊆ t) : hs.extend hst ⊆ t :=
  let ⟨hbt, _hsb, _htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_id_extension hs hst)
  hbt

Subset Property of Linearly Independent Extension

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $s, t \subseteq V$ sets of vectors with $s \subseteq t$. If the vectors in $s$ are linearly independent over $K$ (when considered as a family via the identity map), then the extended set $\text{extend}(hs, hst)$ is a subset of $t$.

LinearIndepOn.subset_extend theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) : s ⊆ hs.extend hst

Full source

theorem LinearIndepOn.subset_extend (hs : LinearIndepOn K id s) (hst : s ⊆ t) : s ⊆ hs.extend hst :=
  let ⟨_hbt, hsb, _htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_id_extension hs hst)
  hsb

Inclusion of Original Set in Its Maximal Linearly Independent Extension

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $s, t \subseteq V$ sets of vectors with $s \subseteq t$. If the vectors in $s$ are linearly independent over $K$ (when considered as a family via the identity map), then $s$ is contained in the maximal linearly independent extension $\text{extend}(s, t)$.

LinearIndepOn.subset_span_extend theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) : t ⊆ span K (hs.extend hst)

Full source

theorem LinearIndepOn.subset_span_extend (hs : LinearIndepOn K id s) (hst : s ⊆ t) :
    t ⊆ span K (hs.extend hst) :=
  let ⟨_hbt, _hsb, htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_id_extension hs hst)
  htb

Span containment of extended linearly independent set

Informal description

Let $K$ be a division ring, $V$ a $K$-module, and $s, t \subseteq V$ sets of vectors such that $s \subseteq t$. If the vectors in $s$ are linearly independent over $K$ (when considered as a family via the identity map), then $t$ is contained in the span of the extended linearly independent set $\text{extend}(hs, hst)$ over $K$, i.e., $t \subseteq \text{span}_K (\text{extend}(hs, hst))$.

LinearIndepOn.span_extend_eq_span theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) : span K (hs.extend hst) = span K t

Full source

theorem LinearIndepOn.span_extend_eq_span (hs : LinearIndepOn K id s) (hst : s ⊆ t) :
    span K (hs.extend hst) = span K t :=
  le_antisymm (span_mono (hs.extend_subset hst)) (span_le.2 (hs.subset_span_extend hst))

Span Equality for Extended Linearly Independent Set

Informal description

Let $K$ be a division ring and $V$ a $K$-module. Given subsets $s \subseteq t \subseteq V$ such that the vectors in $s$ are linearly independent over $K$ (when considered via the identity map), the span of the extended linearly independent set $\text{extend}(s, t)$ over $K$ equals the span of $t$ over $K$, i.e., \[ \text{span}_K (\text{extend}(s, t)) = \text{span}_K t. \]

LinearIndepOn.linearIndepOn_extend theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) : LinearIndepOn K id (hs.extend hst)

Full source

theorem LinearIndepOn.linearIndepOn_extend (hs : LinearIndepOn K id s) (hst : s ⊆ t) :
    LinearIndepOn K id (hs.extend hst) :=
  let ⟨_hbt, _hsb, _htb, hli⟩ := Classical.choose_spec (exists_linearIndepOn_id_extension hs hst)
  hli

Linear Independence of Extended Set in Module over Division Ring

Informal description

Let $K$ be a division ring and $V$ a $K$-module. Given subsets $s \subseteq t \subseteq V$ such that the vectors in $s$ are linearly independent over $K$ (when considered via the identity map), then the extended set $\text{extend}(s, t)$ is also linearly independent over $K$.

exists_of_linearIndepOn_of_finite_span theorem

 {t : Finset V} (hs : LinearIndepOn K id s) (hst : s ⊆ (span K ↑t : Submodule K V)) :
  ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Full source

theorem exists_of_linearIndepOn_of_finite_span {t : Finset V}
    (hs : LinearIndepOn K id s) (hst : s ⊆ (span K ↑t : Submodule K V)) :
    ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card := by
  classical
  have :
    ∀ t : Finset V,
      ∀ s' : Finset V,
        ↑s' ⊆ s →
          s ∩ ↑t = ∅ →
            s ⊆ (span K ↑(s' ∪ t) : Submodule K V) →
              ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
    fun t =>
    Finset.induction_on t
      (fun s' hs' _ hss' =>
        have : s = ↑s' := eq_of_linearIndepOn_id_of_span_subtype hs hs' <| by simpa using hss'
        ⟨s', by simp [this]⟩)
      fun b₁ t hb₁t ih s' hs' hst hss' =>
      have hb₁s : b₁ ∉ s := fun h => by
        have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
        rwa [hst] at this
      have hb₁s' : b₁ ∉ s' := fun h => hb₁s <| hs' h
      have hst : s ∩ ↑t = ∅ :=
        eq_empty_of_subset_empty <|
          -- Porting note: `-inter_subset_left, -subset_inter_iff` required.
          Subset.trans
            (by simp [inter_subset_inter, Subset.refl, -inter_subset_left, -subset_inter_iff])
            (le_of_eq hst)
      Classical.by_cases (p := s ⊆ (span K ↑(s' ∪ t) : Submodule K V))
        (fun this =>
          let ⟨u, hust, hsu, Eq⟩ := ih _ hs' hst this
          have hb₁u : b₁ ∉ u := fun h => (hust h).elim hb₁s hb₁t
          ⟨insert b₁ u, by simp [insert_subset_insert hust], Subset.trans hsu (by simp), by
            simp [Eq, hb₁t, hb₁s', hb₁u]⟩)
        fun this =>
        let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this
        have hb₂t' : b₂ ∉ s' ∪ t := fun h => hb₂t <| subset_span h
        have : s ⊆ (span K ↑(insert b₂ s' ∪ t) : Submodule K V) := fun b₃ hb₃ => by
          have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]
          have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
          have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
          have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
          rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃
        let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset_iff, hb₂s, hs']) hst this
        ⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu,
          by simp [eq, hb₂t', hb₁t, hb₁s']⟩
  have eq : ((t.filter fun x => x ∈ s) ∪ t.filter fun x => x ∉ s) = t := by
    ext1 x
    by_cases x ∈ s <;> simp [*]
  apply
    Exists.elim
      (this (t.filter fun x => x ∉ s) (t.filter fun x => x ∈ s) (by simp [Set.subset_def])
        (by simp +contextual [Set.ext_iff]) (by rwa [eq]))
  intro u h
  exact
    ⟨u, Subset.trans h.1 (by simp +contextual [subset_def, and_imp, or_imp]),
      h.2.1, by simp only [h.2.2, eq]⟩

Existence of Finite Spanning Subset Preserving Cardinality under Linear Independence

Informal description

Let $K$ be a division ring and $V$ a module over $K$. Given a linearly independent subset $s \subseteq V$ and a finite subset $t \subseteq V$ such that $s$ is contained in the span of $t$, there exists a finite subset $t' \subseteq V$ satisfying: 1. $t' \subseteq s \cup t$, 2. $s \subseteq t'$, and 3. The cardinality of $t'$ equals that of $t$.

exists_finite_card_le_of_finite_of_linearIndependent_of_span theorem

 (ht : t.Finite) (hs : LinearIndepOn K id s) (hst : s ⊆ span K t) : ∃ h : s.Finite, h.toFinset.card ≤ ht.toFinset.card

Full source

theorem exists_finite_card_le_of_finite_of_linearIndependent_of_span (ht : t.Finite)
    (hs : LinearIndepOn K id s) (hst : s ⊆ span K t) :
    ∃ h : s.Finite, h.toFinset.card ≤ ht.toFinset.card :=
  have : s ⊆ (span K ↑ht.toFinset : Submodule K V) := by simpa
  let ⟨u, _hust, hsu, Eq⟩ := exists_of_linearIndepOn_of_finite_span hs this
  have : s.Finite := u.finite_toSet.subset hsu
  ⟨this, by rw [← Eq]; exact Finset.card_le_card <| Finset.coe_subset.mp <| by simp [hsu]⟩

Finite cardinality bound for linearly independent subsets in a span

Informal description

Let $K$ be a division ring and $V$ a module over $K$. Given a finite subset $t \subseteq V$ and a linearly independent subset $s \subseteq V$ such that $s$ is contained in the span of $t$, there exists a finite subset $s' \subseteq s$ with $s'$ having cardinality at most that of $t$.

Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Main statements

TODO

Tags