From 99aa0286eba4a56fdd855591e457efc039d0abba Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Mon, 4 Apr 2022 11:55:40 -0400 Subject: [PATCH 1/4] feat(group_theory/torsion): extension closedness, and torsion scalars over modules Co-authored by: Alex J. Best --- src/group_theory/torsion.lean | 43 ++++++++++++++++++++++++++++++++--- 1 file changed, 40 insertions(+), 3 deletions(-) diff --git a/src/group_theory/torsion.lean b/src/group_theory/torsion.lean index 893f8ad6ddd02..8a48ac1b6ce10 100644 --- a/src/group_theory/torsion.lean +++ b/src/group_theory/torsion.lean @@ -73,15 +73,31 @@ lemma is_torsion.subgroup (tG : is_torsion G) (H : subgroup G) : is_torsion 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) := +lemma is_torsion.quotient_group [N.normal] (tG : is_torsion G) : is_torsion (G ⧸ N) := λ h, quotient_group.induction_on' h $ λ g, (tG g).quotient N g +/-- 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 (tN : is_torsion N) [N.normal] (tGN : is_torsion (G ⧸ N)) : +is_torsion G := λ g, begin + obtain ⟨ngn, ngnpos, hngn⟩ := (is_of_fin_order_iff_pow_eq_one _).mp (tGN g), + lift g ^ ngn to N using (quotient_group.eq_one_iff _).mp hngn with gn, + obtain ⟨nn, nnpos, hnn⟩ := (is_of_fin_order_iff_pow_eq_one _).mp (tN gn), + exact ((is_of_fin_order_iff_pow_eq_one _).mpr + ⟨ngn * nn, mul_pos ngnpos nnpos, by rw [pow_mul, ←h, ←subgroup.coe_pow, hnn, subgroup.coe_one]⟩) +end + +/-- An iff version of `is_torsion.quotient_group`. -/ +@[to_additive "An iff version of `is_torsion.quotient_group`."] +lemma is_torsion.quotient_group_iff [nN : N.normal] (tN : is_torsion N) : +is_torsion (G ⧸ N) ↔ is_torsion G := ⟨is_torsion.extension_closed tN, is_torsion.quotient_group⟩ + /-- 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 +117,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 (Fq R : Type*) [add_comm_monoid R] + +namespace add_monoid + +/-- A module whose scalars are additively torsion is additively torsion. -/ +lemma is_torsion.module_of_torsion [semiring Fq] [module Fq R] (tFq : is_torsion Fq) : +is_torsion R := λ 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 (tFq 1), + exact ⟨n, npos, by simp only [nsmul_eq_smul_cast Fq _ 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 Fq] [fintype Fq] [module Fq R] : is_torsion R := +(is_add_torsion_of_fintype : is_torsion Fq).module_of_torsion _ _ + +end add_monoid + +end module section comm_monoid From 218a0909573fffda4b2b0d7278917fde4b530dd1 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Mon, 18 Apr 2022 20:58:49 -0400 Subject: [PATCH 2/4] Generalize to 'morally-quotient' quotients. --- src/group_theory/torsion.lean | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/group_theory/torsion.lean b/src/group_theory/torsion.lean index 8a48ac1b6ce10..81326758f0954 100644 --- a/src/group_theory/torsion.lean +++ b/src/group_theory/torsion.lean @@ -64,7 +64,7 @@ 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} {GmodN : Type*} [group GmodN] /-- Subgroups of torsion groups are torsion groups. -/ @[to_additive "Subgroups of additive torsion groups are additive torsion groups."] @@ -79,13 +79,16 @@ lemma is_torsion.quotient_group [N.normal] (tG : is_torsion G) : is_torsion (G /-- 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 (tN : is_torsion N) [N.normal] (tGN : is_torsion (G ⧸ N)) : -is_torsion G := λ g, begin - obtain ⟨ngn, ngnpos, hngn⟩ := (is_of_fin_order_iff_pow_eq_one _).mp (tGN g), - lift g ^ ngn to N using (quotient_group.eq_one_iff _).mp hngn with gn, +lemma is_torsion.extension_closed + {f : G →* GmodN} {hN : N = f.ker} (tGmodN : is_torsion GmodN) (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 (tGmodN $ 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 ((is_of_fin_order_iff_pow_eq_one _).mpr - ⟨ngn * nn, mul_pos ngnpos nnpos, by rw [pow_mul, ←h, ←subgroup.coe_pow, hnn, subgroup.coe_one]⟩) + exact ⟨ngn * nn, mul_pos ngnpos nnpos, by rw [pow_mul, ←h, ←subgroup.coe_pow, + hnn, subgroup.coe_one]⟩ end /-- An iff version of `is_torsion.quotient_group`. -/ From 1772349eb693becb8708e98e38f76c0098c7bb50 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Mon, 18 Apr 2022 20:59:03 -0400 Subject: [PATCH 3/4] Generalize the quotient lemmas a bit more still. --- src/group_theory/order_of_element.lean | 33 +++++++++++++++-------- src/group_theory/torsion.lean | 37 ++++++++++++++++---------- 2 files changed, 45 insertions(+), 25 deletions(-) diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean index 0601bcbd24878..e98eea37dcfbe 100644 --- a/src/group_theory/order_of_element.lean +++ b/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⟩ diff --git a/src/group_theory/torsion.lean b/src/group_theory/torsion.lean index 81326758f0954..64f6d6ccc3816 100644 --- a/src/group_theory/torsion.lean +++ b/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,26 +64,32 @@ noncomputable def is_torsion.group [monoid G] (tG : is_torsion G) : group G := section group -variables [group G] {N : subgroup G} {GmodN : Type*} [group GmodN] +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 - -/-- 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 [N.normal] (tG : is_torsion G) : is_torsion (G ⧸ N) := -λ h, quotient_group.induction_on' h $ λ g, (tG g).quotient N g +λ 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_surj_hom + "The image of a surjective additive torsion group homomorphism is torsion."] +lemma is_torsion.of_surj_hom {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 →* GmodN} {hN : N = f.ker} (tGmodN : is_torsion GmodN) (tN : is_torsion N) : + {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 (tGmodN $ f g), + 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), @@ -91,10 +97,13 @@ lemma is_torsion.extension_closed hnn, subgroup.coe_one]⟩ end -/-- An iff version of `is_torsion.quotient_group`. -/ -@[to_additive "An iff version of `is_torsion.quotient_group`."] -lemma is_torsion.quotient_group_iff [nN : N.normal] (tN : is_torsion N) : -is_torsion (G ⧸ N) ↔ is_torsion G := ⟨is_torsion.extension_closed tN, is_torsion.quotient_group⟩ +/-- 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 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_surj_hom hf tG⟩ /-- If a group exponent exists, the group is torsion. -/ @[to_additive exponent_exists.is_add_torsion From 0ba7e49f52c0dd1d7e65fb3188bc3a6943d4235c Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Thu, 21 Apr 2022 06:30:19 -0400 Subject: [PATCH 4/4] Better naming. Co-authored by: Johan Commelin --- src/group_theory/torsion.lean | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/group_theory/torsion.lean b/src/group_theory/torsion.lean index 64f6d6ccc3816..82aff19a43d52 100644 --- a/src/group_theory/torsion.lean +++ b/src/group_theory/torsion.lean @@ -72,9 +72,9 @@ lemma is_torsion.subgroup (tG : is_torsion G) (H : subgroup G) : is_torsion 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_surj_hom +@[to_additive add_is_torsion.of_surjective "The image of a surjective additive torsion group homomorphism is torsion."] -lemma is_torsion.of_surj_hom {f : G →* H} (hf : function.surjective f) (tG : is_torsion G) : +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, @@ -99,11 +99,11 @@ end /-- 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 torsion iff the group is torsion."] + "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_surj_hom hf tG⟩ +⟨λ 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 @@ -132,20 +132,20 @@ end group section module -- A (semi/)ring of scalars and a commutative monoid of elements -variables (Fq R : Type*) [add_comm_monoid R] +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 Fq] [module Fq R] (tFq : is_torsion Fq) : -is_torsion R := λ 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 (tFq 1), - exact ⟨n, npos, by simp only [nsmul_eq_smul_cast Fq _ f, ←nsmul_one, hn, zero_smul]⟩, +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 Fq] [fintype Fq] [module Fq R] : is_torsion R := -(is_add_torsion_of_fintype : is_torsion Fq).module_of_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