English
With the appropriate freeness and finiteness hypotheses, the finite rank of the quotient S/I over F equals the sum of the finite ranks of the quotients by the Smith coefficients, over all i.
Русский
С учетом условий, ранг фактор-модуля S/I над F равен сумме рангов соответствующих фактор-модулей по коэффициентам Смита.
LaTeX
$$$\operatorname{finrank}_F(S/I)=\sum_{i} \operatorname{finrank}_F\left(R/\langle I.smithCoeffs(b,hI,i)\rangle\right)$$$
Lean4
theorem finrank_quotient_eq_sum {ι} [Fintype ι] (b : Basis ι R S) [Nontrivial F]
[∀ i, Module.Free F (R ⧸ span ({I.smithCoeffs b hI i} : Set R))]
[∀ i, Module.Finite F (R ⧸ span ({I.smithCoeffs b hI i} : Set R))] :
Module.finrank F (S ⧸ I) = ∑ i, Module.finrank F (R ⧸ span ({I.smithCoeffs b hI i} : Set R)) := by
-- slow, and dot notation doesn't work
rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b hI, Module.finrank_directSum]
