English
If a submodule S of a finite-dimensional space V has the same finrank as V, then S is the whole space.
Русский
Если подпространство S под конечномерного пространства V имеет такую же размерность, как V, то S равно всему пространству.
LaTeX
$$$ S = \top \quad \text{iff} \quad \ finrank\ K\ S = \ finrank\ K\ V $$$
Lean4
/-- If a submodule has maximal dimension in a finite-dimensional space, then it is equal to the
whole space. -/
theorem _root_.Submodule.eq_top_of_finrank_eq [FiniteDimensional K V] {S : Submodule K V}
(h : finrank K S = finrank K V) : S = ⊤ :=
by
set bS := Basis.ofVectorSpace K S with bS_eq
have : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K S) := by
simpa [bS] using bS.linearIndependent.linearIndepOn_id.image (f := Submodule.subtype S) (by simp)
set b := Basis.extend this with b_eq
letI i1 : Fintype (this.extend _) :=
(LinearIndependent.set_finite_of_isNoetherian (by simpa [b] using b.linearIndependent)).fintype
letI i2 : Fintype (((↑) : S → V) '' Basis.ofVectorSpaceIndex K S) :=
(LinearIndependent.set_finite_of_isNoetherian this).fintype
letI i3 : Fintype (Basis.ofVectorSpaceIndex K S) :=
(LinearIndependent.set_finite_of_isNoetherian (by simpa [bS] using bS.linearIndependent)).fintype
have : (↑) '' Basis.ofVectorSpaceIndex K S = this.extend (Set.subset_univ _) :=
Set.eq_of_subset_of_card_le (this.subset_extend _)
(by
rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ← finrank_eq_card_basis b,
h])
rw [← b.span_eq, b_eq, Basis.coe_extend, Subtype.range_coe, ← this, ← Submodule.coe_subtype, span_image]
have := bS.span_eq
rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this
rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]
