Documentation

Mathlib.GroupTheory.Torsion

Torsion groups #

This file defines torsion groups, i.e. groups where all elements have finite order.

Main definitions #

Implementation #

All torsion monoids are really groups (which is proven here as Monoid.IsTorsion.group), but since the definition can be stated on monoids it is implemented on monoid to match other declarations in the group theory library.

Tags #

periodic group, aperiodic group, torsion subgroup, torsion abelian group

Future work #

A predicate on an additive monoid saying that all elements are of finite order.

Equations
Instances For
    def Monoid.IsTorsion (G : Type u_1) [Monoid G] :

    A predicate on a monoid saying that all elements are of finite order.

    Equations
    Instances For
      @[simp]

      An additive monoid is not a torsion monoid if it has an element of infinite order.

      @[simp]

      A monoid is not a torsion monoid if it has an element of infinite order.

      theorem IsTorsion.addGroup.proof_2 {G : Type u_1} [AddMonoid G] :
      ∀ (a : G), zsmulRec 0 a = zsmulRec 0 a
      noncomputable def IsTorsion.addGroup {G : Type u_1} [AddMonoid G] (tG : AddMonoid.IsTorsion G) :

      Torsion additive monoids are really additive groups

      Equations
      Instances For
        theorem IsTorsion.addGroup.proof_5 {G : Type u_1} [AddMonoid G] (tG : AddMonoid.IsTorsion G) (g : G) :
        -g + g = 0
        theorem IsTorsion.addGroup.proof_4 {G : Type u_1} [AddMonoid G] :
        ∀ (n : ) (a : G), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
        theorem IsTorsion.addGroup.proof_1 {G : Type u_1} [AddMonoid G] :
        ∀ (a b : G), a - b = a - b
        theorem IsTorsion.addGroup.proof_3 {G : Type u_1} [AddMonoid G] :
        ∀ (n : ) (a : G), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a
        noncomputable def IsTorsion.group {G : Type u_1} [Monoid G] (tG : Monoid.IsTorsion G) :

        Torsion monoids are really groups.

        Equations
        Instances For

          Subgroups of additive torsion groups are additive torsion groups.

          theorem IsTorsion.subgroup {G : Type u_1} [Group G] (tG : Monoid.IsTorsion G) (H : Subgroup G) :

          Subgroups of torsion groups are torsion groups.

          theorem AddIsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} (hf : Function.Surjective f) (tG : AddMonoid.IsTorsion G) :

          The image of a surjective additive torsion group homomorphism is torsion.

          theorem IsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} (hf : Function.Surjective f) (tG : Monoid.IsTorsion G) :

          The image of a surjective torsion group homomorphism is torsion.

          theorem AddIsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hN : N = AddMonoidHom.ker f) (tH : AddMonoid.IsTorsion H) (tN : AddMonoid.IsTorsion N) :

          Additive torsion groups are closed under extensions.

          theorem IsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hN : N = MonoidHom.ker f) (tH : Monoid.IsTorsion H) (tN : Monoid.IsTorsion N) :

          Torsion groups are closed under extensions.

          theorem AddIsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hf : Function.Surjective f) (hN : N = AddMonoidHom.ker f) (tN : AddMonoid.IsTorsion N) :

          The image of a quotient is additively torsion iff the group is torsion.

          theorem IsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hf : Function.Surjective f) (hN : N = MonoidHom.ker f) (tN : Monoid.IsTorsion N) :

          The image of a quotient is torsion iff the group is torsion.

          If a group exponent exists, the group is additively torsion.

          If a group exponent exists, the group is torsion.

          The group exponent exists for any bounded additive torsion group.

          theorem IsTorsion.exponentExists {G : Type u_1} [Group G] (tG : Monoid.IsTorsion G) (bounded : Set.Finite (Set.range fun (g : G) => orderOf g)) :

          The group exponent exists for any bounded torsion group.

          Finite additive groups are additive torsion groups.

          Finite groups are torsion groups.

          A module whose scalars are additively torsion is additively torsion.

          A module with a finite ring of scalars is additively torsion.

          The torsion submonoid of an additive commutative monoid.

          Equations
          Instances For

            The torsion submonoid of a commutative monoid.

            (Note that by Monoid.IsTorsion.group torsion monoids are truthfully groups.)

            Equations
            Instances For
              abbrev AddCommMonoid.addTorsion.isTorsion.match_1 {G : Type u_1} [AddCommMonoid G] (motive : (AddCommMonoid.addTorsion G)Prop) :
              ∀ (x : (AddCommMonoid.addTorsion G)), (∀ (x : G) (n : ) (npos : n > 0) (hn : Function.IsPeriodicPt (fun (x_1 : G) => x + x_1) n 0), motive { val := x, property := })motive x
              Equations
              • =
              Instances For

                Additive torsion submonoids are additively torsion.

                Torsion submonoids are torsion.

                theorem AddCommMonoid.primaryComponent.proof_2 (G : Type u_1) [AddCommMonoid G] (p : ) :
                ∃ (n : ), addOrderOf 0 = p ^ n
                theorem AddCommMonoid.primaryComponent.proof_1 (G : Type u_1) [AddCommMonoid G] (p : ) [hp : Fact (Nat.Prime p)] :
                ∀ {a b : G}, a {g : G | ∃ (n : ), addOrderOf g = p ^ n}b {g : G | ∃ (n : ), addOrderOf g = p ^ n}∃ (k : ), addOrderOf (a + b) = p ^ k

                The p-primary component is the submonoid of elements with additive order prime-power of p.

                Equations
                Instances For
                  @[simp]
                  theorem AddCommMonoid.primaryComponent_coe (G : Type u_1) [AddCommMonoid G] (p : ) [hp : Fact (Nat.Prime p)] :
                  (AddCommMonoid.primaryComponent G p) = {g : G | ∃ (n : ), addOrderOf g = p ^ n}
                  @[simp]
                  theorem CommMonoid.primaryComponent_coe (G : Type u_1) [CommMonoid G] (p : ) [hp : Fact (Nat.Prime p)] :
                  (CommMonoid.primaryComponent G p) = {g : G | ∃ (n : ), orderOf g = p ^ n}
                  def CommMonoid.primaryComponent (G : Type u_1) [CommMonoid G] (p : ) [hp : Fact (Nat.Prime p)] :

                  The p-primary component is the submonoid of elements with order prime-power of p.

                  Equations
                  Instances For

                    Elements of the p-primary component have additive order p^n for some n

                    Elements of the p-primary component have order p^n for some n.

                    The p- and q-primary components are disjoint for p ≠ q.

                    theorem CommMonoid.primaryComponent.disjoint {G : Type u_1} [CommMonoid G] {p : } [hp : Fact (Nat.Prime p)] {p' : } [hp' : Fact (Nat.Prime p')] (hne : p p') :

                    The p- and q-primary components are disjoint for p ≠ q.

                    @[simp]

                    The additive torsion submonoid of an additive torsion monoid is .

                    @[simp]

                    The torsion submonoid of a torsion monoid is .

                    An additive torsion monoid is isomorphic to its torsion submonoid.

                    Equations
                    Instances For

                      A torsion monoid is isomorphic to its torsion submonoid.

                      Equations
                      Instances For
                        theorem AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe {G : Type u_1} [AddCommMonoid G] (tG : AddMonoid.IsTorsion G) (a : G) :
                        (AddEquiv.symm (AddMonoid.IsTorsion.torsionAddEquiv tG)) a = { val := ((AddEquiv.symm AddSubmonoid.topEquiv) a), property := }
                        theorem Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe {G : Type u_1} [CommMonoid G] (tG : Monoid.IsTorsion G) (a : G) :
                        (MulEquiv.symm (Monoid.IsTorsion.torsionMulEquiv tG)) a = { val := ((MulEquiv.symm Submonoid.topEquiv) a), property := }

                        Additive torsion submonoids of an additive torsion submonoid are isomorphic to the submonoid.

                        Equations
                        Instances For

                          Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.

                          Equations
                          Instances For

                            The torsion subgroup of an additive abelian group.

                            Equations
                            Instances For
                              theorem AddCommGroup.torsion.proof_1 (G : Type u_1) [AddCommGroup G] :
                              ∀ {x : G}, x (AddCommMonoid.addTorsion G).carrierIsOfFinAddOrder (-x)

                              The torsion subgroup of an abelian group.

                              Equations
                              Instances For

                                The additive torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.

                                The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.

                                abbrev AddCommGroup.primaryComponent.match_1 (G : Type u_1) [AddCommGroup G] (p : ) [hp : Fact (Nat.Prime p)] {g : G} :
                                let __src := AddCommMonoid.primaryComponent G p; ∀ (motive : g __src.carrierProp) (x : g __src.carrier), (∀ (n : ) (hn : addOrderOf g = p ^ n), motive )motive x
                                Equations
                                • =
                                Instances For

                                  The p-primary component is the subgroup of elements with additive order prime-power of p.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem CommGroup.primaryComponent_coe (G : Type u_1) [CommGroup G] (p : ) [hp : Fact (Nat.Prime p)] :
                                    (CommGroup.primaryComponent G p) = {g : G | ∃ (n : ), orderOf g = p ^ n}
                                    @[simp]
                                    theorem AddCommGroup.primaryComponent_coe (G : Type u_1) [AddCommGroup G] (p : ) [hp : Fact (Nat.Prime p)] :
                                    (AddCommGroup.primaryComponent G p) = {g : G | ∃ (n : ), addOrderOf g = p ^ n}
                                    def CommGroup.primaryComponent (G : Type u_1) [CommGroup G] (p : ) [hp : Fact (Nat.Prime p)] :

                                    The p-primary component is the subgroup of elements with order prime-power of p.

                                    Equations
                                    Instances For

                                      The p-primary component is a p group.

                                      A predicate on an additive monoid saying that only 0 is of finite order.

                                      Equations
                                      Instances For

                                        A predicate on a monoid saying that only 1 is of finite order.

                                        Equations
                                        Instances For
                                          @[simp]

                                          An additive monoid is not torsion free if any nontrivial element has finite order.

                                          @[simp]

                                          A nontrivial monoid is not torsion-free if any nontrivial element has finite order.

                                          A nontrivial additive torsion group is not torsion-free.

                                          A nontrivial torsion group is not torsion-free.

                                          A nontrivial torsion-free additive group is not torsion.

                                          A nontrivial torsion-free group is not torsion.

                                          Subgroups of additive torsion-free groups are additively torsion-free.

                                          Subgroups of torsion-free groups are torsion-free.

                                          theorem AddMonoid.IsTorsionFree.prod {η : Type u_3} {Gs : ηType u_4} [(i : η) → AddGroup (Gs i)] (tfGs : ∀ (i : η), AddMonoid.IsTorsionFree (Gs i)) :
                                          AddMonoid.IsTorsionFree ((i : η) → Gs i)

                                          Direct products of additive torsion free groups are torsion free.

                                          theorem IsTorsionFree.prod {η : Type u_3} {Gs : ηType u_4} [(i : η) → Group (Gs i)] (tfGs : ∀ (i : η), Monoid.IsTorsionFree (Gs i)) :
                                          Monoid.IsTorsionFree ((i : η) → Gs i)

                                          Direct products of torsion free groups are torsion free.

                                          Quotienting a group by its additive torsion subgroup yields an additive torsion free group.

                                          Quotienting a group by its torsion subgroup yields a torsion free group.