Theorems · Theorem · commutative algebra

Submodule.basis_of_pid_aux

∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [IsPrincipalIdealRing R] [IsDomain R] [Finite ι] {O : Type u_4}
  [inst_4 : AddCommGroup O] [inst_5 : Module R O] (M N : Submodule R O) (b'M : Module.Basis ι R ↥M),
  N ≠ ⊥ →
    N ≤ M →
      ∃ y ∈ M,
        ∃ a,
          a • y ∈ N ∧
            ∃ M' ≤ M,
              ∃ N' ≤ N,
                N' ≤ M' ∧
                  (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                    (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                      ∀ (n' : ℕ) (bN' : Module.Basis (Fin n') R ↥N'),
                        ∃ bN,
                          ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Module.Basis (Fin m') R ↥M'),
                            ∃ (hnm : n' + 1 ≤ m' + 1),
                              ∃ bM,
                                ∀ (as : Fin n' → R),
                                  (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                    ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))

The induction hypothesis of Submodule.basisOfPid and Submodule.smithNormalForm. Basically, it says: let N ≤ M be a pair of submodules, then we can find a pair of submodules N' ≤ M' of strictly smaller rank, whose basis we can extend to get a basis of N and M. Moreover, if the basis for M' is up to scalars a basis for N', then the basis we find for M is up to scalars a basis for N. For basis_of_pid we only need the first half and can fix M = ⊤, for smith_normal_form we need the full statement, but must also feed in a basis for M using basis_of_pid to keep the induction going.

Defined in

Mathlib.LinearAlgebra.FreeModule.PID

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsPrincipalIdealRingIsDomainFiniteAddCommGroupModule