English
Let ι be finite and b a basis of a free R-module M. If an R-submodule N has the same R-rank as M and the Smith-coefficients generate finite, free quotients over F, then the F-rank of the quotient M/N equals the sum of the F-ranks of the quotients by the principal ideals generated by the Smith coefficients.
Русский
Пусть ι конечен и b — базис свободного R-модуля M. Если заключение N имеет ту же ранговую размерность, что и M, и соответствующие коэффициенты Смита порождают конечные свободные фактор-модульe над F, то F-рангкк (M/N) равен сумме F-рангов (M /⟨smithCoeffs b h i⟩) по i.
LaTeX
$$$\operatorname{finrank}_F(M/N)=\sum_{i} \operatorname{finrank}_F\bigl(R/\langle\operatorname{smithCoeffs}(b,h,i)\rangle\bigr)$$$
Lean4
theorem finrank_quotient_eq_sum {ι} [Fintype ι] (b : Basis ι R M) [Nontrivial F]
(h : Module.finrank R N = Module.finrank R M)
[∀ i, Module.Free F (R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R))]
[∀ i, Module.Finite F (R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R))] :
Module.finrank F (M ⧸ N) = ∑ i, Module.finrank F (R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R)) := by
rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b h, Module.finrank_directSum]
