quotientEquivDirectSum — Mathlib

English

Decompose M/N as a direct sum of cyclic modules, using a scalars F and smith normal form data.

Русский

Разложить M/N как прямую сумму циклических модулей с использованием скалярного поля F и данных smith normal form.

LaTeX

$$$$ (M / N) \cong \bigoplus_{i} R / ( \mathrm{Ideal.span}( \{ \mathrm{smithNormalFormCoeffs}_i \} )). $$$$

Lean4

/-- Decompose `M⧸N` as a direct sum of cyclic `R`-modules
  (quotients by the ideals generated by Smith coefficients of `N`). -/
noncomputable def quotientEquivDirectSum (h : Module.finrank R N = Module.finrank R M) :
    (M ⧸ N) ≃ₗ[F] ⨁ i, R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R) :=
  by
  haveI := Fintype.ofFinite ι
  exact ((N.quotientEquivPiSpan b _).restrictScalars F).trans (DirectSum.linearEquivFunOnFintype _ _ _).symm

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