English
A basis is a maximal linearly independent subset of the ambient module.
Русский
Базис есть максимальная линейно независимая подзадача модуля.
LaTeX
$$$b.\\text{linearIndependent.Maximal}$$$
Lean4
/-- Any basis is a maximal linear independent set.
-/
theorem maximal [Nontrivial R] (b : Basis ι R M) : b.linearIndependent.Maximal := fun w hi h => by
-- If `w` is strictly bigger than `range b`,
apply le_antisymm h
intro x p
by_contra q
have e := b.linearCombination_repr x
let u : ι ↪ w := ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r => b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
simp_rw [Finsupp.linearCombination_apply] at e
change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)), ← Finsupp.linearCombination_apply] at e
refine hi.linearCombination_ne_of_notMem_support _ ?_ e
simp only [Finset.mem_map, Finsupp.support_embDomain]
rintro ⟨j, -, W⟩
simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
apply q ⟨j, W⟩
