English
Let R be a local ring that is finite free over S, and p its maximal ideal. Then finrank of the quotient modules satisfies finrank (R ⧸ p) (S ⧸ pS) = finrank R S.
Русский
Пусть R — локальное кольцо, конечная свободная над R алгебра S (с пике максимальной идеальной p). Тогда размерности по модулю удовлетворяют: finrank_{R/p}(S/pS) = finrank_R(S).
LaTeX
$$$\\operatorname{finrank} (R/\\mathfrak p) (S/\\mathfrak p S) = \\operatorname{finrank} R S$$$
Lean4
theorem finrank_quotient_map : finrank (R ⧸ p) (S ⧸ pS) = finrank R S := by
classical
have : Module.Finite R (S ⧸ pS) :=
Module.Finite.of_surjective (IsScalarTower.toAlgHom R S (S ⧸ pS)).toLinearMap
(Ideal.Quotient.mk_surjective (I := pS))
have : Module.Finite (R ⧸ p) (S ⧸ pS) := Module.Finite.of_restrictScalars_finite R _ _
apply le_antisymm
· let b := Module.Free.chooseBasis R S
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
apply finrank_le_of_span_eq_top
rw [Set.range_comp]
apply (quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq
· let b := Module.Free.chooseBasis (R ⧸ p) (S ⧸ pS)
choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
refine finrank_le_of_span_eq_top (v := b') ?_
apply (quotient_span_eq_top_iff_span_eq_top _).mp
rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']
exact b.span_eq
