Theorems · Definition · commutative algebra

Submodule.smithNormalFormCoeffs

{ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [IsPrincipalIdealRing R] →
                {N : Submodule R M} → [Finite ι] → Module.Basis ι R M → Module.finrank R ↥N = Module.finrank R M → ι → R

If M is finite free over a PID R, then for any submodule N of the same rank, we can find basis for M and N with the same indexing such that the inclusion map is a square diagonal matrix; these are the entries of the diagonal matrix. See: * Submodule.smithNormalFormTopBasis for the basis on M, * Submodule.smithNormalFormBotBasis for the basis on N, * Submodule.smithNormalFormBotBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Defined in

Mathlib.LinearAlgebra.FreeModule.PID

Cited by

6 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleIsDomainIsPrincipalIdealRingFinite