Theorems · Theorem · commutative algebra

Submodule.exists_smith_normal_form_of_le

∀ {ι : 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] [Finite ι] (b : Module.Basis ι R M) (N O : Submodule R M),
  N ≤ O → ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))

If M is finite free over a PID R, then any submodule N is free and we can find a basis for M and N such that the inclusion map is a diagonal matrix in Smith normal form. See Submodule.smithNormalFormOfLE for a version of this theorem that returns a Basis.SmithNormalForm. This is a strengthening of Submodule.basisOfPidOfLE.

Defined in

Mathlib.LinearAlgebra.FreeModule.PID

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleIsDomainIsPrincipalIdealRingFinite