feat(group_theory/torsion): extension closedness, and torsion scalars…

… in modules (#13172)


Co-authored by: Alex J. Best <alex.j.best@gmail.com>

src/group_theory/order_of_element.lean

@@ -68,23 +68,34 @@ 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.-/
+/-- Elements of finite order are of finite order in submonoids.-/
 @[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) :
+lemma is_of_fin_order_iff_coe (H : submonoid 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 }
 
-/-- 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⟩⟩,
+/-- The image of an element of finite order has finite order. -/
+@[to_additive add_monoid_hom.is_of_fin_order
+  "The image of an element of finite additive order has finite additive order."]
+lemma monoid_hom.is_of_fin_order
+  {H : Type v} [monoid H] (f : G →* H) {x : G} (h : is_of_fin_order x) :
+  is_of_fin_order $ f x :=
+(is_of_fin_order_iff_pow_eq_one _).mpr $ begin
+  rcases (is_of_fin_order_iff_pow_eq_one _).mp h with ⟨n, npos, hn⟩,
+  exact ⟨n, npos, by rw [←f.map_pow, hn, f.map_one]⟩,
+end
+
+/-- If a direct product has finite order then so does each component. -/
+@[to_additive "If a direct product has finite additive order then so does each component."]
+lemma is_of_fin_order.apply
+  {η : Type*} {Gs : η → Type*} [∀ i, monoid (Gs i)] {x : Π i, Gs i} (h : is_of_fin_order x) :
+∀ i, is_of_fin_order (x i) := begin
+  rcases (is_of_fin_order_iff_pow_eq_one _).mp h with ⟨n, npos, hn⟩,
+  exact λ _, (is_of_fin_order_iff_pow_eq_one _).mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩,
 end
 
-/-- 1 is of finite order in any group. -/
-@[to_additive "0 is of finite order in any additive group."]
+/-- 1 is of finite order in any monoid. -/
+@[to_additive "0 is of finite order in any additive monoid."]
 lemma is_of_fin_order_one : is_of_fin_order (1 : G) :=
 (is_of_fin_order_iff_pow_eq_one 1).mpr ⟨1, _root_.one_pos, one_pow 1⟩
 

src/group_theory/torsion.lean

@@ -37,7 +37,7 @@ periodic group, torsion subgroup, torsion abelian group
 * torsion-free groups
 -/
 
-variable {G : Type*}
+variables {G H : Type*}
 
 namespace monoid
 
@@ -64,24 +64,52 @@ noncomputable def is_torsion.group [monoid G] (tG : is_torsion G) : group G :=
 
 section group
 
-variables [group G] {N : subgroup G}
+variables [group G] {N : subgroup G} [group H]
 
 /-- 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
+λ h, (is_of_fin_order_iff_coe H.to_submonoid h).mpr $ tG h
+
+/-- The image of a surjective torsion group homomorphism is torsion. -/
+@[to_additive add_is_torsion.of_surjective
+  "The image of a surjective additive torsion group homomorphism is torsion."]
+lemma is_torsion.of_surjective {f : G →* H} (hf : function.surjective f) (tG : is_torsion G) :
+  is_torsion H :=
+λ h, begin
+  obtain ⟨g, hg⟩ := hf h,
+  rw ←hg,
+  exact f.is_of_fin_order (tG g),
+end
+
+/-- Torsion groups are closed under extensions. -/
+@[to_additive add_is_torsion.extension_closed
+  "Additive torsion groups are closed under extensions."]
+lemma is_torsion.extension_closed
+  {f : G →* H} (hN : N = f.ker) (tH : is_torsion H) (tN : is_torsion N) :
+  is_torsion G :=
+λ g, (is_of_fin_order_iff_pow_eq_one _).mpr $ begin
+  obtain ⟨ngn, ngnpos, hngn⟩ := (is_of_fin_order_iff_pow_eq_one _).mp (tH $ f g),
+  have hmem := f.mem_ker.mpr ((f.map_pow g ngn).trans hngn),
+  lift g ^ ngn to N using hN.symm ▸ hmem with gn,
+  obtain ⟨nn, nnpos, hnn⟩ := (is_of_fin_order_iff_pow_eq_one _).mp (tN gn),
+  exact ⟨ngn * nn, mul_pos ngnpos nnpos, by rw [pow_mul, ←h, ←subgroup.coe_pow,
+                                                hnn, subgroup.coe_one]⟩
+end
 
-/-- 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
+/-- The image of a quotient is torsion iff the group is torsion. -/
+@[to_additive add_is_torsion.quotient_iff
+  "The image of a quotient is additively torsion iff the group is torsion."]
+lemma is_torsion.quotient_iff
+  {f : G →* H} (hf : function.surjective f) (hN : N = f.ker) (tN : is_torsion N) :
+  is_torsion H ↔ is_torsion G :=
+⟨λ tH, is_torsion.extension_closed hN tH tN, λ tG, is_torsion.of_surjective hf tG⟩
 
 /-- If a group exponent exists, the group is torsion. -/
 @[to_additive exponent_exists.is_add_torsion
   "If a group exponent exists, the group is additively torsion."]
-lemma exponent_exists.is_torsion (h : exponent_exists G) : is_torsion G := begin
+lemma exponent_exists.is_torsion (h : exponent_exists G) : is_torsion G := λ 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
 
@@ -101,6 +129,27 @@ exponent_exists.is_torsion $ exponent_exists_iff_ne_zero.mpr exponent_ne_zero_of
 
 end group
 
+section module
+
+-- A (semi/)ring of scalars and a commutative monoid of elements
+variables (R M : Type*) [add_comm_monoid M]
+
+namespace add_monoid
+
+/-- A module whose scalars are additively torsion is additively torsion. -/
+lemma is_torsion.module_of_torsion [semiring R] [module R M] (tR : is_torsion R) :
+is_torsion M := λ f, (is_of_fin_add_order_iff_nsmul_eq_zero _).mpr $ begin
+  obtain ⟨n, npos, hn⟩ := (is_of_fin_add_order_iff_nsmul_eq_zero _).mp (tR 1),
+  exact ⟨n, npos, by simp only [nsmul_eq_smul_cast R _ f, ←nsmul_one, hn, zero_smul]⟩,
+end
+
+/-- A module with a finite ring of scalars is additively torsion. -/
+lemma is_torsion.module_of_fintype [ring R] [fintype R] [module R M] : is_torsion M :=
+(is_add_torsion_of_fintype : is_torsion R).module_of_torsion _ _
+
+end add_monoid
+
+end module
 
 section comm_monoid