Documentation

Mathlib.Algebra.Module.Torsion

Torsion submodules #

Main definitions #

Main statements #

Notation #

Tags #

Torsion, submodule, module, quotient

@[simp]
theorem Ideal.torsionOf_carrier (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
def Ideal.torsionOf (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :

The torsion ideal of x, containing all a such that a • x = 0.

Equations
Instances For
    @[simp]
    theorem Ideal.torsionOf_zero (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
    @[simp]
    theorem Ideal.mem_torsionOf_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (a : R) :
    a Ideal.torsionOf R M x a x = 0
    @[simp]
    theorem Ideal.torsionOf_eq_top_iff (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (m : M) :
    theorem Ideal.CompleteLattice.Independent.linear_independent' {ι : Type u_3} {R : Type u_4} {M : Type u_5} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hv : CompleteLattice.Independent fun (i : ι) => Submodule.span R {v i}) (h_ne_zero : ∀ (i : ι), Ideal.torsionOf R M (v i) = ) :

    See also CompleteLattice.Independent.linearIndependent which provides the same conclusion but requires the stronger hypothesis NoZeroSMulDivisors R M.

    noncomputable def Ideal.quotTorsionOfEquivSpanSingleton (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] (x : M) :

    The span of x in M is isomorphic to R quotiented by the torsion ideal of x.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Ideal.quotTorsionOfEquivSpanSingleton_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (x : M) (a : R) :
      @[simp]
      theorem Submodule.torsionBy_carrier (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :
      def Submodule.torsionBy (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :

      The a-torsion submodule for a in R, containing all elements x of M such that a • x = 0.

      Equations
      Instances For
        @[simp]
        theorem Submodule.torsionBySet_carrier (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) :
        (Submodule.torsionBySet R M s) = ys, (DistribMulAction.toLinearMap R M y) ⁻¹' {0}
        def Submodule.torsionBySet (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) :

        The submodule containing all elements x of M such that a • x = 0 for all a in s.

        Equations
        Instances For
          @[simp]
          theorem Submodule.torsion'AddSubMonoid_coe (M : Type u_2) [AddCommMonoid M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] :
          (Submodule.torsion'AddSubMonoid M S) = {x : M | ∃ (a : S), a x = 0}

          The additive submonoid of all elements x of M such that a • x = 0 for some a in S.

          Equations
          Instances For
            @[simp]
            theorem Submodule.torsion'_carrier (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :
            (Submodule.torsion' R M S) = {x : M | ∃ (a : S), a x = 0}
            def Submodule.torsion' (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :

            The S-torsion submodule, containing all elements x of M such that a • x = 0 for some a in S.

            Equations
            Instances For
              @[reducible, inline]
              abbrev Submodule.torsion (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :

              The torsion submodule, containing all elements x of M such that a • x = 0 for some non-zero-divisor a in R.

              Equations
              Instances For
                @[reducible, inline]
                abbrev Module.IsTorsionBy (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :

                An a-torsion module is a module where every element is a-torsion.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Module.IsTorsionBySet (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) :

                  A module where every element is a-torsion for all a in s.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Module.IsTorsion' (M : Type u_2) [AddCommMonoid M] (S : Type u_3) [SMul S M] :

                    An S-torsion module is a module where every element is a-torsion for some a in S.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev Module.IsTorsion (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :

                      A torsion module is a module where every element is a-torsion for some non-zero-divisor a.

                      Equations
                      Instances For
                        @[simp]
                        theorem Submodule.smul_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : (Submodule.torsionBy R M a)) :
                        a x = 0
                        @[simp]
                        theorem Submodule.smul_coe_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : (Submodule.torsionBy R M a)) :
                        a x = 0
                        @[simp]
                        theorem Submodule.mem_torsionBy_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : M) :
                        @[simp]
                        theorem Submodule.mem_torsionBySet_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (x : M) :
                        x Submodule.torsionBySet R M s ∀ (a : s), a x = 0

                        Torsion by a set is torsion by the ideal generated by it.

                        theorem Submodule.torsionBy_le_torsionBy_of_dvd {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (b : R) (dvd : a b) :
                        @[simp]
                        theorem Submodule.torsionBy_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
                        @[simp]
                        theorem Submodule.torsionBySet_univ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

                        An a-torsion module is a module whose a-torsion submodule is the full space.

                        theorem Submodule.torsionBy_isTorsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :

                        The a-torsion submodule is an a-torsion module.

                        @[simp]
                        theorem Submodule.torsion_gc (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :
                        GaloisConnection Submodule.annihilator fun (I : (Ideal R)ᵒᵈ) => Submodule.torsionBySet R M (OrderDual.ofDual I)
                        theorem Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {p : ιIdeal R} {S : Finset ι} (hp : (S).Pairwise fun (i j : ι) => p i p j = ) :
                        iS, Submodule.torsionBySet R M (p i) = Submodule.torsionBySet R M (iS, p i)
                        theorem Submodule.supIndep_torsionBySet_ideal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {p : ιIdeal R} {S : Finset ι} (hp : (S).Pairwise fun (i j : ι) => p i p j = ) :
                        S.SupIndep fun (i : ι) => Submodule.torsionBySet R M (p i)
                        theorem Submodule.iSup_torsionBy_eq_torsionBy_prod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ιR} (hq : (S).Pairwise (IsCoprime on q)) :
                        iS, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (iS, q i)
                        theorem Submodule.supIndep_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ιR} (hq : (S).Pairwise (IsCoprime on q)) :
                        S.SupIndep fun (i : ι) => Submodule.torsionBy R M (q i)
                        theorem Submodule.torsionBySet_isInternal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [DecidableEq ι] {S : Finset ι} {p : ιIdeal R} (hp : (S).Pairwise fun (i j : ι) => p i p j = ) (hM : Module.IsTorsionBySet R M (iS, p i)) :
                        DirectSum.IsInternal fun (i : { x : ι // x S }) => Submodule.torsionBySet R M (p i)

                        If the p i are pairwise coprime, a ⨅ i, p i-torsion module is the internal direct sum of its p i-torsion submodules.

                        theorem Submodule.torsionBy_isInternal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [DecidableEq ι] {S : Finset ι} {q : ιR} (hq : (S).Pairwise (IsCoprime on q)) (hM : Module.IsTorsionBy R M (iS, q i)) :
                        DirectSum.IsInternal fun (i : { x : ι // x S }) => Submodule.torsionBy R M (q i)

                        If the q i are pairwise coprime, a ∏ i, q i-torsion module is the internal direct sum of its q i-torsion submodules.

                        def Module.IsTorsionBySet.hasSMul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M I) :
                        SMul (R I) M

                        can't be an instance because hM can't be inferred

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev Module.IsTorsionBy.hasSMul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (hM : Module.IsTorsionBy R M r) :
                          SMul (R Ideal.span {r}) M

                          can't be an instance because hM can't be inferred

                          Equations
                          • hM.hasSMul = .hasSMul
                          Instances For
                            @[simp]
                            theorem Module.IsTorsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M I) (b : R) (x : M) :
                            @[simp]
                            theorem Module.IsTorsionBy.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (hM : Module.IsTorsionBy R M r) (b : R) (x : M) :
                            def Module.IsTorsionBySet.module {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M I) :
                            Module (R I) M

                            An (R ⧸ I)-module is an R-module which IsTorsionBySet R M I.

                            Equations
                            Instances For
                              instance Module.IsTorsionBySet.isScalarTower {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : Module.IsTorsionBySet R M I) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
                              IsScalarTower S (R I) M
                              Equations
                              • =
                              @[reducible, inline]
                              abbrev Module.IsTorsionBy.module {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (hM : Module.IsTorsionBy R M r) :

                              An (R ⧸ Ideal.span {r})-module is an R-module for which IsTorsionBy R M r.

                              Equations
                              • hM.module = .module
                              Instances For

                                Any module is also a module over the quotient of the ring by the annihilator. Not an instance because it causes synthesis failures / timeouts.

                                Equations
                                • Module.quotientAnnihilator = .module
                                Instances For
                                  theorem Module.isTorsionBy_quotient_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) :
                                  Module.IsTorsionBy R (M N) r ∀ (x : M), r x N
                                  theorem Module.IsTorsionBy.quotient {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) {r : R} (h : Module.IsTorsionBy R M r) :
                                  theorem Module.isTorsionBySet_quotient_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (s : Set R) :
                                  Module.IsTorsionBySet R (M N) s ∀ (x : M), rs, r x N
                                  theorem Module.IsTorsionBySet.quotient {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) {s : Set R} (h : Module.IsTorsionBySet R M s) :
                                  instance Module.instQuotientIdealSubmoduleHSMulTop {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
                                  Module (R I) (M I )
                                  Equations
                                  theorem Module.Quotient.mk_smul_mk {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (r : R) (m : M) :
                                  @[simp]
                                  theorem Submodule.torsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (b : R) (x : (Submodule.torsionBySet R M I)) :
                                  instance Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
                                  Equations
                                  • =
                                  instance Submodule.instModuleQuotientTorsionBy {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) :

                                  The a-torsion submodule as an (R ⧸ R∙a)-module.

                                  Equations
                                  @[simp]
                                  theorem Submodule.torsionBy.mk_ideal_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) (b : R) (x : (Submodule.torsionBy R M a)) :
                                  theorem Submodule.torsionBy.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) (b : R) (x : (Submodule.torsionBy R M a)) :
                                  Equations
                                  • =

                                  Given an R-module M and an element a in R, submodules of the a-torsion submodule of M do not depend on whether we take scalars to be R or R ⧸ R ∙ a.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem Submodule.mem_torsion'_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] (x : M) :
                                    x Submodule.torsion' R M S ∃ (a : S), a x = 0
                                    theorem Submodule.mem_torsion_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) :
                                    x Submodule.torsion R M ∃ (a : (nonZeroDivisors R)), a x = 0
                                    @[simp]
                                    theorem Submodule.instSMulSubtypeMemTorsion'_smul_coe {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (x : (Submodule.torsion' R M S)) :
                                    (s x) = s x
                                    instance Submodule.instSMulSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :
                                    Equations
                                    Equations
                                    • =

                                    An S-torsion module is a module whose S-torsion submodule is the full space.

                                    The S-torsion submodule is an S-torsion module.

                                    @[simp]

                                    The torsion submodule of the torsion submodule (viewed as a module) is the full torsion module.

                                    The torsion submodule is always a torsion module.

                                    theorem Submodule.coe_torsion_eq_annihilator_ne_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] [Nontrivial R] :
                                    (Submodule.torsion R M) = {x : M | (Submodule.span R {x}).annihilator }

                                    A module over a domain has NoZeroSMulDivisors iff its torsion submodule is trivial.

                                    @[simp]

                                    Quotienting by the torsion submodule gives a torsion-free module.

                                    theorem Submodule.isTorsion'_powers_iff {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (p : R) :
                                    Module.IsTorsion' M (Submonoid.powers p) ∀ (x : M), ∃ (n : ), p ^ n x = 0
                                    def Submodule.pOrder {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] {p : R} (hM : Module.IsTorsion' M (Submonoid.powers p)) (x : M) [(n : ) → Decidable (p ^ n x = 0)] :

                                    In a p ^ ∞-torsion module (that is, a module where all elements are cancelled by scalar multiplication by some power of p), the smallest n such that p ^ n • x = 0.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Submodule.pow_pOrder_smul {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] {p : R} (hM : Module.IsTorsion' M (Submonoid.powers p)) (x : M) [(n : ) → Decidable (p ^ n x = 0)] :
                                      p ^ Submodule.pOrder hM x x = 0
                                      theorem Submodule.exists_isTorsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [(x : M) → Decidable (x = 0)] {p : R} (hM : Module.IsTorsion' M (Submonoid.powers p)) (d : ) (hd : d 0) (s : Fin dM) (hs : Submodule.span R (Set.range s) = ) :
                                      ∃ (j : Fin d), Module.IsTorsionBy R M (p ^ Submodule.pOrder hM (s j))