English
Over any ring R satisfying the strong rank condition, if b is an infinite basis of M and v is linearly independent in M with v maximal, then the cardinality of the index set κ of v equals the cardinality of the basis index set ι of b.
Русский
Пусть R удовлетворяет условию сильной ранговости. Если b — бесконечный базис M, и v линейно независим в M и максимален, то кардинальность индексов κ равна кардинальности индексов ι базиса b.
LaTeX
$$$|\\kappa| = |\\iota|$$$
Lean4
/-- Over any ring `R` satisfying the strong rank condition,
if `b` is an infinite basis for a module `M`,
then every maximal linearly independent set has the same cardinality as `b`.
This proof (along with some of the lemmas above) comes from
[Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973]
-/
theorem maximal_linearIndependent_eq_infinite_basis {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M)
(i : LinearIndependent R v) (m : i.Maximal) : #κ = #ι :=
by
apply le_antisymm
· exact linearIndependent_le_basis b v i
· haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R
exact infinite_basis_le_maximal_linearIndependent b v i m
