Skip to content

Commit

Permalink
feat: extend a linearly independent family to a basis contained in a …
Browse files Browse the repository at this point in the history
…set spanning the space (#17102)

If `s` is a family of linearly independent vectors contained in a set `t` spanning `V`, `extendLe` is a basis of `V` containing `s` and contained in `t`.
Specialize it for the case where `s` is empty.
  • Loading branch information
Etienne committed Oct 8, 2024
1 parent f681278 commit 196892d
Showing 1 changed file with 55 additions and 0 deletions.
55 changes: 55 additions & 0 deletions Mathlib/LinearAlgebra/Basis/VectorSpace.lean
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,61 @@ theorem subset_extend {s : Set V} (hs : LinearIndependent K ((↑) : s → V)) :
s ⊆ hs.extend (Set.subset_univ _) :=
hs.subset_extend _

/-- If `s` is a family of linearly independent vectors contained in a set `t` spanning `V`,
then one can get a basis of `V` containing `s` and contained in `t`. -/
noncomputable def extendLe (hs : LinearIndependent K ((↑) : s → V))
(hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
Basis (hs.extend hst) K V :=
Basis.mk
(@LinearIndependent.restrict_of_comp_subtype _ _ _ id _ _ _ _ (hs.linearIndependent_extend _))
(le_trans ht <| Submodule.span_le.2 <| by simpa using hs.subset_span_extend hst)

theorem extendLe_apply_self (hs : LinearIndependent K ((↑) : s → V))
(hst : s ⊆ t) (ht : ⊤ ≤ span K t) (x : hs.extend hst) :
Basis.extendLe hs hst ht x = x :=
Basis.mk_apply _ _ _

@[simp]
theorem coe_extendLe (hs : LinearIndependent K ((↑) : s → V))
(hst : s ⊆ t) (ht : ⊤ ≤ span K t) : ⇑(Basis.extendLe hs hst ht) = ((↑) : _ → _) :=
funext (extendLe_apply_self hs hst ht)

theorem range_extendLe (hs : LinearIndependent K ((↑) : s → V))
(hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
range (Basis.extendLe hs hst ht) = hs.extend hst := by
rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]

theorem subset_extendLe (hs : LinearIndependent K ((↑) : s → V))
(hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
s ⊆ range (Basis.extendLe hs hst ht) :=
(range_extendLe hs hst ht).symm ▸ hs.subset_extend hst

theorem extendLe_subset (hs : LinearIndependent K ((↑) : s → V))
(hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
range (Basis.extendLe hs hst ht) ⊆ t :=
(range_extendLe hs hst ht).symm ▸ hs.extend_subset hst

/-- If a set `s` spans the space, this is a basis contained in `s`. -/
noncomputable def ofSpan (hs : ⊤ ≤ span K s) :
Basis ((linearIndependent_empty K V).extend (empty_subset s)) K V :=
extendLe (linearIndependent_empty K V) (empty_subset s) hs

theorem ofSpan_apply_self (hs : ⊤ ≤ span K s)
(x : (linearIndependent_empty K V).extend (empty_subset s)) :
Basis.ofSpan hs x = x :=
extendLe_apply_self (linearIndependent_empty K V) (empty_subset s) hs x

@[simp]
theorem coe_ofSpan (hs : ⊤ ≤ span K s) : ⇑(ofSpan hs) = ((↑) : _ → _) :=
funext (ofSpan_apply_self hs)

theorem range_ofSpan (hs : ⊤ ≤ span K s) :
range (ofSpan hs) = (linearIndependent_empty K V).extend (empty_subset s) := by
rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]

theorem ofSpan_subset (hs : ⊤ ≤ span K s) : range (ofSpan hs) ⊆ s :=
extendLe_subset (linearIndependent_empty K V) (empty_subset s) hs

section

variable (K V)
Expand Down

0 comments on commit 196892d

Please sign in to comment.