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) :
      (Ideal.quotTorsionOfEquivSpanSingleton R M x) (Submodule.Quotient.mk a) = a { val := x, property := }
      @[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) = ⋂ y ∈ s, (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 w) [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 w) [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 w) [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]
              def 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]
                def 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]
                  def 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]
                    def 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]
                      def 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 : Set.Pairwise S fun (i j : ι) => p i p j = ) :
                        ⨆ i ∈ S, Submodule.torsionBySet R M (p i) = Submodule.torsionBySet R M (⨅ i ∈ S, 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 : Set.Pairwise S fun (i j : ι) => p i p j = ) :
                        Finset.SupIndep S 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 : Set.Pairwise (S) (IsCoprime on q)) :
                        ⨆ i ∈ S, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (Finset.prod S fun (i : ι) => 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 : Set.Pairwise (S) (IsCoprime on q)) :
                        Finset.SupIndep S 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 : Set.Pairwise S fun (i j : ι) => p i p j = ) (hM : Module.IsTorsionBySet R M (⨅ i ∈ S, 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 : Set.Pairwise (S) (IsCoprime on q)) (hM : Module.IsTorsionBy R M (Finset.prod S fun (i : ι) => 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
                          @[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) :
                          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
                            • =

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

                            Equations
                            Instances For
                              @[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.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)) :

                              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]

                                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.

                                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))