English
If there exists a finite basis h: ι → S over R for a module M, then finrank_R(M) equals the cardinality of ι, i.e., finrank_R(M) = card ι.
Русский
Если существует конечный базис h: ι → S над R для модуля M, то finrank_R(M) = card ι.
LaTeX
$$\\operatorname{finrank}_R(M) = |\\iota|$$
Lean4
/-- If `S` a module-finite free `R`-algebra, then the `R`-rank of a nonzero `R`-free
ideal `I` of `S` is the same as the rank of `S`. -/
theorem rank_eq {R S : Type*} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S] [Algebra R S] {n m : Type*}
[Fintype n] [Fintype m] (b : Basis n R S) {I : Ideal S} (hI : I ≠ ⊥) (c : Basis m R I) :
Fintype.card m = Fintype.card n :=
by
obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr hI)
have : LinearIndependent R fun i => b i • a :=
by
have hb := b.linearIndependent
rw [Fintype.linearIndependent_iff] at hb ⊢
intro g hg
apply hb g
simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg
exact hg.resolve_right ha
exact
le_antisymm
(b.card_le_card_of_linearIndependent
(c.linearIndependent.map' (Submodule.subtype I)
((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective)))
(c.card_le_card_of_linearIndependent this)
