quotientEquivDirectSum — Mathlib

English

For a subring extension with SmithNormalForm, S/ I decomposes as a direct sum of the quotients by principal ideals generated by Smith coefficients.

Русский

Разложение S/ I по прямому сумме фактор-модулей по каждому коэффициенту Смитa.

LaTeX

$$$(S/I) \cong_F \bigoplus_{i} R/\langle I.smithCoeffs(b,hI,i)\rangle$$$

Lean4

/-- Decompose `S⧸I` as a direct sum of cyclic `R`-modules
  (quotients by the ideals generated by Smith coefficients of `I`). -/
noncomputable def quotientEquivDirectSum : (S ⧸ I) ≃ₗ[F] ⨁ i, R ⧸ span ({I.smithCoeffs b hI i} : Set R) :=
  Submodule.quotientEquivDirectSum F b (N := (I.restrictScalars R)) <| finrank_eq_finrank b I hI

Похожие утверждения