feat(group_theory/torsion): define torsion groups (#11850)

I grepped for torsion group and didn't find anything -- hopefully adding this makes sense here.

Author: Julian

src/group_theory/exponent.lean

@@ -64,14 +64,18 @@ if h : exponent_exists G then nat.find h else 0
 variable {G}
 
 @[to_additive]
-lemma exponent_eq_zero_iff : exponent G = 0 ↔ ¬ exponent_exists G :=
+lemma exponent_exists_iff_ne_zero : exponent_exists G ↔ exponent G ≠ 0 :=
 begin
   rw [exponent],
   split_ifs,
   { simp [h, @not_lt_zero' ℕ] }, --if this isn't done this way, `to_additive` freaks
-  { tauto }
+  { tauto },
 end
 
+@[to_additive]
+lemma exponent_eq_zero_iff : exponent G = 0 ↔ ¬ exponent_exists G := 
+by simp only [exponent_exists_iff_ne_zero, not_not]
+
 @[to_additive]
 lemma exponent_eq_zero_of_order_zero {g : G} (hg : order_of g = 0) : exponent G = 0 :=
 exponent_eq_zero_iff.mpr $ λ ⟨n, hn, hgn⟩, order_of_eq_zero_iff'.mp hg n hn $ hgn g

src/group_theory/order_of_element.lean

@@ -8,6 +8,7 @@ import algebra.iterate_hom
 import algebra.pointwise
 import dynamics.periodic_pts
 import group_theory.coset
+import group_theory.quotient_group
 
 /-!
 # Order of an element
@@ -68,6 +69,23 @@ lemma is_of_fin_order_iff_pow_eq_one (x : G) :
   is_of_fin_order x ↔ ∃ n, 0 < n ∧ x ^ n = 1 :=
 by { convert iff.rfl, simp [is_periodic_pt_mul_iff_pow_eq_one] }
 
+/-- Elements of finite order are of finite order in subgroups.-/
+@[to_additive is_of_fin_add_order_iff_coe]
+lemma is_of_fin_order_iff_coe {G : Type u} [group G] (H : subgroup G) (x : H) :
+  is_of_fin_order x ↔ is_of_fin_order (x : G) :=
+by { rw [is_of_fin_order_iff_pow_eq_one, is_of_fin_order_iff_pow_eq_one], norm_cast }
+
+variables 
+
+/-- Elements of finite order are of finite order in quotient groups.-/
+@[to_additive is_of_fin_add_order_iff_quotient]
+lemma is_of_fin_order.quotient {G : Type u} [group G] (N : subgroup G) [N.normal] (x : G) :
+  is_of_fin_order x → is_of_fin_order (x : G ⧸ N) := begin
+  rw [is_of_fin_order_iff_pow_eq_one, is_of_fin_order_iff_pow_eq_one],
+  rintros ⟨n, ⟨npos, hn⟩⟩,
+  exact ⟨n, ⟨npos, (quotient_group.con N).eq.mpr $ hn ▸ (quotient_group.con N).eq.mp rfl⟩⟩,
+end
+
 end is_of_fin_order
 
 /-- `order_of x` is the order of the element `x`, i.e. the `n ≥ 1`, s.t. `x ^ n = 1` if it exists.

src/group_theory/torsion.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2022 Julian Berman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julian Berman
+-/
+
+import group_theory.exponent
+import group_theory.order_of_element
+import group_theory.quotient_group
+
+/-!
+# Torsion groups
+
+This file defines torsion groups, i.e. groups where all elements have finite order.
+
+## Main definitions
+
+* `monoid.is_torsion` is a predicate asserting a monoid `G` is a torsion monoid, i.e. that all
+  elements are of finite order. Torsion groups are also known as periodic groups.
+* `add_monoid.is_torsion` the additive version of `monoid.is_torsion`.
+
+## Future work
+
+* Define `tor G` for the torsion subgroup of a group
+* torsion-free groups
+-/
+
+universe u
+
+variable {G : Type u}
+
+open_locale classical
+
+namespace monoid
+
+variables (G) [monoid G]
+
+/--A predicate on a monoid saying that all elements are of finite order.-/
+@[to_additive "A predicate on an additive monoid saying that all elements are of finite order."]
+def is_torsion := ∀ g : G, is_of_fin_order g
+
+end monoid
+
+open monoid
+
+variables [group G] {N : subgroup G}
+
+/--Subgroups of torsion groups are torsion groups. -/
+@[to_additive "Subgroups of additive torsion groups are additive torsion groups."]
+lemma is_torsion.subgroup (tG : is_torsion G) (H : subgroup G) : is_torsion H :=
+λ h, (is_of_fin_order_iff_coe _ h).mpr $ tG h
+
+/--Quotient groups of torsion groups are torsion groups. -/
+@[to_additive "Quotient groups of additive torsion groups are additive torsion groups."]
+lemma is_torsion.quotient_group [nN : N.normal] (tG : is_torsion G) : is_torsion (G ⧸ N) :=
+λ h, quotient_group.induction_on' h $ λ g, (tG g).quotient N g
+
+/--If a group exponent exists, the group is torsion. -/
+@[to_additive exponent_exists.is_add_torsion]
+lemma exponent_exists.is_torsion (h : exponent_exists G) : is_torsion G := begin
+  obtain ⟨n, npos, hn⟩ := h,
+  intro g,
+  exact (is_of_fin_order_iff_pow_eq_one g).mpr ⟨n, npos, hn g⟩,
+end
+
+/--The group exponent exists for any bounded torsion group. -/
+@[to_additive is_add_torsion.exponent_exists]
+lemma is_torsion.exponent_exists
+  (tG : is_torsion G) (bounded : (set.range (λ g : G, order_of g)).finite) :
+  exponent_exists G :=
+exponent_exists_iff_ne_zero.mpr $
+  (exponent_ne_zero_iff_range_order_of_finite (λ g, order_of_pos' (tG g))).mpr bounded
+
+/--Finite groups are torsion groups.-/
+@[to_additive is_add_torsion_of_fintype]
+lemma is_torsion_of_fintype [fintype G] : is_torsion G :=
+exponent_exists.is_torsion $ exponent_exists_iff_ne_zero.mpr exponent_ne_zero_of_fintype