Theorems · Definition · commutative algebra

Submodule.smithNormalFormTopBasis

{ι : 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 → Module.Basis ι R M

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; this is the basis for M. See: * Submodule.smithNormalFormBotBasis for the basis on N, * Submodule.smithNormalFormCoeffs for the entries of the diagonal matrix * Submodule.smithNormalFormBotBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Defined in

Mathlib.LinearAlgebra.FreeModule.PID

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleIsDomainIsPrincipalIdealRingFinite