Documentation

Mathlib.LinearAlgebra.FreeModule.PID

Free modules over PID #

A free R-module M is a module with a basis over R, equivalently it is an R-module linearly equivalent to ι →₀ R for some ι.

This file proves a submodule of a free R-module of finite rank is also a free R-module of finite rank, if R is a principal ideal domain (PID), i.e. we have instances [IsDomain R] [IsPrincipalIdealRing R]. We express "free R-module of finite rank" as a module M which has a basis b : ι → R, where ι is a Fintype. We call the cardinality of ι the rank of M in this file; it would be equal to finrank R M if R is a field and M is a vector space.

Main results #

In this section, M is a free and finitely generated R-module, and N is a submodule of M.

Tags #

free module, finitely generated module, rank, structure theorem

theorem eq_bot_of_generator_maximal_map_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_1} (b : Basis ι R M) {N : Submodule R M} {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N) [(Submodule.map ϕ N).IsPrincipal] (hgen : Submodule.IsPrincipal.generator (Submodule.map ϕ N) = 0) :
N =
theorem eq_bot_of_generator_maximal_submoduleImage_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_1} {N : Submodule R M} {O : Submodule R M} (b : Basis ι R O) (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N) [(ϕ.submoduleImage N).IsPrincipal] (hgen : Submodule.IsPrincipal.generator (ϕ.submoduleImage N) = 0) :
N =
theorem generator_maximal_submoduleImage_dvd {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Submodule R M} {O : Submodule R M} (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N) [(ϕ.submoduleImage N).IsPrincipal] (y : M) (yN : y N) (ϕy_eq : ϕ y, = Submodule.IsPrincipal.generator (ϕ.submoduleImage N)) (ψ : O →ₗ[R] R) :
Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ψ y,
theorem Submodule.basis_of_pid_aux {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] {O : Type u_4} [AddCommGroup O] [Module R O] (M : Submodule R O) (N : Submodule R O) (b'M : Basis ι R M) (N_bot : N ) (N_le_M : N M) :
yM, ∃ (a : R), a y N M'M, N'N, N' M' (∀ (c : R), zM', c y + z = 0c = 0) (∀ (c : R), zN', c a y + z = 0c = 0) ∀ (n' : ) (bN' : Basis (Fin n') R N'), ∃ (bN : Basis (Fin (n' + 1)) R N), ∀ (m' : ) (hn'm' : n' m') (bM' : Basis (Fin m') R M'), ∃ (hnm : n' + 1 m' + 1) (bM : Basis (Fin (m' + 1)) R M), ∀ (as : Fin n'R), (∀ (i : Fin n'), (bN' i) = as i (bM' (Fin.castLE hn'm' i)))∃ (as' : Fin (n' + 1)R), ∀ (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.

theorem Submodule.nonempty_basis_of_pid {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (b : Basis ι R M) (N : Submodule R M) :
∃ (n : ), Nonempty (Basis (Fin n) R N)

A submodule of a free R-module of finite rank is also a free R-module of finite rank, if R is a principal ideal domain.

This is a lemma to make the induction a bit easier. To actually access the basis, see Submodule.basisOfPid.

See also the stronger version Submodule.smithNormalForm.

noncomputable def Submodule.basisOfPid {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (b : Basis ι R M) (N : Submodule R M) :
(n : ) × Basis (Fin n) R N

A submodule of a free R-module of finite rank is also a free R-module of finite rank, if R is a principal ideal domain.

See also the stronger version Submodule.smithNormalForm.

Equations
Instances For
    theorem Submodule.basisOfPid_bot {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (b : Basis ι R M) :
    noncomputable def Submodule.basisOfPidOfLE {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] {N : Submodule R M} {O : Submodule R M} (hNO : N O) (b : Basis ι R O) :
    (n : ) × Basis (Fin n) R N

    A submodule inside a free R-submodule of finite rank is also a free R-module of finite rank, if R is a principal ideal domain.

    See also the stronger version Submodule.smithNormalFormOfLE.

    Equations
    Instances For
      noncomputable def Submodule.basisOfPidOfLESpan {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] {b : ιM} (hb : LinearIndependent R b) {N : Submodule R M} (le : N Submodule.span R (Set.range b)) :
      (n : ) × Basis (Fin n) R N

      A submodule inside the span of a linear independent family is a free R-module of finite rank, if R is a principal ideal domain.

      Equations
      Instances For
        noncomputable def Module.basisOfFiniteTypeTorsionFree {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Fintype ι] {s : ιM} (hs : Submodule.span R (Set.range s) = ) [NoZeroSMulDivisors R M] :
        (n : ) × Basis (Fin n) R M

        A finite type torsion free module over a PID admits a basis.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Module.free_of_finite_type_torsion_free {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Finite ι] {s : ιM} (hs : Submodule.span R (Set.range s) = ) [NoZeroSMulDivisors R M] :
          noncomputable def Module.basisOfFiniteTypeTorsionFree' {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Module.Finite R M] [NoZeroSMulDivisors R M] :
          (n : ) × Basis (Fin n) R M

          A finite type torsion free module over a PID admits a basis.

          Equations
          Instances For
            instance instFreeSubtypeMemIdealOfFiniteOfNoZeroSMulDivisors {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [Algebra R S] {I : Ideal S} [hI₁ : Module.Finite R I] [hI₂ : NoZeroSMulDivisors R I] :
            Equations
            • =
            structure Basis.SmithNormalForm {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) (ι : Type u_4) (n : ) :
            Type (max (max u_2 u_3) u_4)

            A Smith normal form basis for a submodule N of a module M consists of bases for M and N such that the inclusion map N → M can be written as a (rectangular) matrix with a along the diagonal: in Smith normal form.

            • bM : Basis ι R M

              The basis of M.

            • bN : Basis (Fin n) R N

              The basis of N.

            • f : Fin n ι

              The mapping between the vectors of the bases.

            • a : Fin nR

              The (diagonal) entries of the matrix.

            • snf : ∀ (i : Fin n), (self.bN i) = self.a i self.bM (self.f i)

              The SNF relation between the vectors of the bases.

            Instances For
              theorem Basis.SmithNormalForm.snf {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Submodule R M} {ι : Type u_4} {n : } (self : Basis.SmithNormalForm N ι n) (i : Fin n) :
              (self.bN i) = self.a i self.bM (self.f i)

              The SNF relation between the vectors of the bases.

              theorem Basis.SmithNormalForm.repr_eq_zero_of_nmem_range {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) (m : N) {i : ι} (hi : iSet.range snf.f) :
              (snf.bM.repr m) i = 0
              theorem Basis.SmithNormalForm.le_ker_coord_of_nmem_range {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) {i : ι} (hi : iSet.range snf.f) :
              N LinearMap.ker (snf.bM.coord i)
              @[simp]
              theorem Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) (m : N) {i : Fin n} :
              (snf.bM.repr m) (snf.f i) = (snf.bN.repr (snf.a i m)) i
              @[simp]
              theorem Basis.SmithNormalForm.repr_comp_embedding_eq_smul {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) (m : N) :
              (snf.bM.repr m) snf.f = snf.a (snf.bN.repr m)
              @[simp]
              theorem Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) {i : Fin n} :
              snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i snf.bN.coord i
              @[simp]
              theorem Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) [Fintype ι] [DecidableEq ι] (f : M →ₗ[R] M) (hf : ∀ (x : M), f x N) (hf' : optParam (xN, f x N) ) {i : Fin n} :
              (LinearMap.toMatrix snf.bN snf.bN) (f.restrict hf') i i = (LinearMap.toMatrix snf.bM snf.bM) f (snf.f i) (snf.f i)

              Given a Smith-normal-form pair of bases for N ⊆ M, and a linear endomorphism f of M that preserves N, the diagonal of the matrix of the restriction f to N does not depend on which of the two bases for N is used.

              theorem Submodule.exists_smith_normal_form_of_le {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (N : Submodule R M) (O : Submodule R M) (N_le_O : N O) :
              ∃ (n : ) (o : ) (hno : n o) (bO : Basis (Fin o) R O) (bN : Basis (Fin n) R N) (a : Fin nR), ∀ (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.

              noncomputable def Submodule.smithNormalFormOfLE {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (N : Submodule R M) (O : Submodule R M) (N_le_O : N O) :
              (o : ) × (n : ) × Basis.SmithNormalForm (Submodule.comap O.subtype N) (Fin o) n

              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.exists_smith_normal_form_of_le for a version of this theorem that doesn't need to map N into a submodule of O.

              This is a strengthening of Submodule.basisOfPidOfLe.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def Submodule.smithNormalForm {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (N : Submodule R M) :
                (n : ) × Basis.SmithNormalForm N ι n

                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.

                This is a strengthening of Submodule.basisOfPid.

                See also Ideal.smithNormalForm, which moreover proves that the dimension of an ideal is the same as the dimension of the whole ring.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  noncomputable def Ideal.smithNormalForm {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (I : Ideal S) (hI : I ) :

                  If S a finite-dimensional ring extension of a PID R which is free as an R-module, then any nonzero S-ideal I is free as an R-submodule of S, and we can find a basis for S and I such that the inclusion map is a square diagonal matrix.

                  See Ideal.exists_smith_normal_form for a version of this theorem that doesn't need to map I into a submodule of R.

                  This is a strengthening of Submodule.basisOfPid.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem Ideal.exists_smith_normal_form {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (hI : I ) :
                    ∃ (b' : Basis ι R S) (a : ιR) (ab' : Basis ι R I), ∀ (i : ι), (ab' i) = a i b' i

                    If S a finite-dimensional ring extension of a PID R which is free as an R-module, then any nonzero S-ideal I is free as an R-submodule of S, and we can find a basis for S and I such that the inclusion map is a square diagonal matrix.

                    See also Ideal.smithNormalForm for a version of this theorem that returns a Basis.SmithNormalForm.

                    The definitions Ideal.ringBasis, Ideal.selfBasis, Ideal.smithCoeffs are (noncomputable) choices of values for this existential quantifier.

                    noncomputable def Ideal.ringBasis {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (hI : I ) :
                    Basis ι R S

                    If S a finite-dimensional ring extension of a PID R which is free as an R-module, then any nonzero S-ideal I is free as an R-submodule of S, and we can find a basis for S and I such that the inclusion map is a square diagonal matrix; this is the basis for S. See Ideal.selfBasis for the basis on I, see Ideal.smithCoeffs for the entries of the diagonal matrix and Ideal.selfBasis_def for the proof that the inclusion map forms a square diagonal matrix.

                    Equations
                    Instances For
                      noncomputable def Ideal.selfBasis {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (hI : I ) :
                      Basis ι R I

                      If S a finite-dimensional ring extension of a PID R which is free as an R-module, then any nonzero S-ideal I is free as an R-submodule of S, and we can find a basis for S and I such that the inclusion map is a square diagonal matrix; this is the basis for I. See Ideal.ringBasis for the basis on S, see Ideal.smithCoeffs for the entries of the diagonal matrix and Ideal.selfBasis_def for the proof that the inclusion map forms a square diagonal matrix.

                      Equations
                      Instances For
                        noncomputable def Ideal.smithCoeffs {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (hI : I ) :
                        ιR

                        If S a finite-dimensional ring extension of a PID R which is free as an R-module, then any nonzero S-ideal I is free as an R-submodule of S, and we can find a basis for S and I such that the inclusion map is a square diagonal matrix; these are the entries of the diagonal matrix. See Ideal.ringBasis for the basis on S, see Ideal.selfBasis for the basis on I, and Ideal.selfBasis_def for the proof that the inclusion map forms a square diagonal matrix.

                        Equations
                        Instances For
                          @[simp]
                          theorem Ideal.selfBasis_def {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (hI : I ) (i : ι) :
                          ((Ideal.selfBasis b I hI) i) = Ideal.smithCoeffs b I hI i (Ideal.ringBasis b I hI) i

                          If S a finite-dimensional ring extension of a PID R which is free as an R-module, then any nonzero S-ideal I is free as an R-submodule of S, and we can find a basis for S and I such that the inclusion map is a square diagonal matrix.

                          @[simp]
                          theorem Ideal.smithCoeffs_ne_zero {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (hI : I ) (i : ι) :
                          theorem LinearIndependent.restrict_scalars_algebras {R : Type u_1} {S : Type u_2} {M : Type u_3} {ι : Type u_4} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (hinj : Function.Injective (algebraMap R S)) {v : ιM} (li : LinearIndependent S v) :

                          A set of linearly independent vectors in a module M over a semiring S is also linearly independent over a subring R of K.