From e280ac220f168d5bdbfc9c36b760d674b48a0545 Mon Sep 17 00:00:00 2001 From: l_man Date: Tue, 18 Aug 2026 19:37:55 +0200 Subject: [PATCH 1/4] feat(Algebra): add zpow_right_injective MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add the ℤ-specific injectivity lemma and move CharZero.of_isAddTorsionFree to an earlier file, as instructed by the TODO in Algebra.Module.Torsion.Free. --- Mathlib/Algebra/Group/Torsion.lean | 9 +++++++++ Mathlib/Algebra/Module/NatInt.lean | 11 +++++++++++ Mathlib/Algebra/Module/Torsion/Free.lean | 14 -------------- 3 files changed, 20 insertions(+), 14 deletions(-) diff --git a/Mathlib/Algebra/Group/Torsion.lean b/Mathlib/Algebra/Group/Torsion.lean index 8dbf0726d4bbfc..723901b674a061 100644 --- a/Mathlib/Algebra/Group/Torsion.lean +++ b/Mathlib/Algebra/Group/Torsion.lean @@ -87,6 +87,15 @@ lemma IsMulTorsionFree.zpow_eq_one_iff : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by @[to_additive IsAddTorsionFree.zsmul_eq_zero_iff_left] lemma IsMulTorsionFree.zpow_eq_one_iff_right (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 := by simp [*] +@[to_additive zsmul_left_injective] +lemma zpow_right_injective (ha : a ≠ 1) : + Injective fun n : ℤ ↦ a ^ n := by + intro m n h + dsimp at h + apply Int.sub_eq_zero.mp + apply (IsMulTorsionFree.zpow_eq_one_iff_right ha).mp + simp [zpow_sub, h] + @[to_additive] lemma self_eq_inv : a = a⁻¹ ↔ a = 1 := by rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv] @[to_additive] lemma inv_eq_self : a⁻¹ = a ↔ a = 1 := by rw [eq_comm, self_eq_inv] @[to_additive] lemma self_ne_inv : a ≠ a⁻¹ ↔ a ≠ 1 := self_eq_inv.ne diff --git a/Mathlib/Algebra/Module/NatInt.lean b/Mathlib/Algebra/Module/NatInt.lean index 18c0d4c442af54..4d325e6b8c289d 100644 --- a/Mathlib/Algebra/Module/NatInt.lean +++ b/Mathlib/Algebra/Module/NatInt.lean @@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro -/ module +public import Mathlib.Algebra.Group.Torsion public import Mathlib.Algebra.Module.Defs public import Mathlib.Data.Int.Cast.Lemmas @@ -207,6 +208,16 @@ instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCo | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul] | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul] +variable (R M) in +/-- Only a ring of characteristic zero can have a non-trivial module without additive or +scalar torsion. -/ +lemma CharZero.of_isAddTorsionFree [Semiring R] [AddCommGroup M] [Module R M] + [Nontrivial M] [IsAddTorsionFree M] : CharZero R := by + refine ⟨fun {n m h} ↦ ?_⟩ + obtain ⟨x, hx⟩ := exists_ne (0 : M) + replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h] + simpa using zsmul_left_injective hx h + variable (M) in /-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic zero as well. Usually `M` is an `R`-algebra. -/ diff --git a/Mathlib/Algebra/Module/Torsion/Free.lean b/Mathlib/Algebra/Module/Torsion/Free.lean index 5baa8565656825..c148b147cbcfef 100644 --- a/Mathlib/Algebra/Module/Torsion/Free.lean +++ b/Mathlib/Algebra/Module/Torsion/Free.lean @@ -177,17 +177,3 @@ lemma smul_left_injective (hm : m ≠ 0) : ((· • m) : R → M).Injective := b (smul_left_injective _ hm).eq_iff end Ring - -section Semiring -variable (R M) [Semiring R] [AddCommGroup M] [Module R M] - --- TODO: Add a `ℤ`-specific version of `smul_left_injective` and move this lemma to an earlier file. -/-- Only a ring of characteristic zero can have a non-trivial module without additive or -scalar torsion. -/ -lemma CharZero.of_isAddTorsionFree [Nontrivial M] [IsAddTorsionFree M] : CharZero R := by - refine ⟨fun {n m h} ↦ ?_⟩ - obtain ⟨x, hx⟩ := exists_ne (0 : M) - replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h] - simpa using smul_left_injective ℤ hx h - -end Semiring From 19582ce0d11cb2fc6cdecd6764b5a01e30550ffe Mon Sep 17 00:00:00 2001 From: lman310 Date: Tue, 18 Aug 2026 21:20:52 +0200 Subject: [PATCH 2/4] Update Mathlib/Algebra/Group/Torsion.lean Co-authored-by: Felix Pernegger --- Mathlib/Algebra/Group/Torsion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Group/Torsion.lean b/Mathlib/Algebra/Group/Torsion.lean index 723901b674a061..a0927252487355 100644 --- a/Mathlib/Algebra/Group/Torsion.lean +++ b/Mathlib/Algebra/Group/Torsion.lean @@ -89,7 +89,7 @@ lemma IsMulTorsionFree.zpow_eq_one_iff_right (ha : a ≠ 1) : a ^ n = 1 ↔ n = @[to_additive zsmul_left_injective] lemma zpow_right_injective (ha : a ≠ 1) : - Injective fun n : ℤ ↦ a ^ n := by + (a ^ · : ℤ → G).Injective := by intro m n h dsimp at h apply Int.sub_eq_zero.mp From 170d45676ea57958a943080db1e335503ff14ec4 Mon Sep 17 00:00:00 2001 From: lman310 Date: Tue, 18 Aug 2026 21:21:15 +0200 Subject: [PATCH 3/4] Update Mathlib/Algebra/Group/Torsion.lean Co-authored-by: Felix Pernegger --- Mathlib/Algebra/Group/Torsion.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Algebra/Group/Torsion.lean b/Mathlib/Algebra/Group/Torsion.lean index a0927252487355..c439b74629d997 100644 --- a/Mathlib/Algebra/Group/Torsion.lean +++ b/Mathlib/Algebra/Group/Torsion.lean @@ -91,7 +91,6 @@ lemma IsMulTorsionFree.zpow_eq_one_iff_right (ha : a ≠ 1) : a ^ n = 1 ↔ n = lemma zpow_right_injective (ha : a ≠ 1) : (a ^ · : ℤ → G).Injective := by intro m n h - dsimp at h apply Int.sub_eq_zero.mp apply (IsMulTorsionFree.zpow_eq_one_iff_right ha).mp simp [zpow_sub, h] From d00a07ec9ffcbdefdb049f2b17e3911add9dd995 Mon Sep 17 00:00:00 2001 From: lman310 Date: Tue, 18 Aug 2026 21:33:11 +0200 Subject: [PATCH 4/4] Update Mathlib/Algebra/Module/NatInt.lean Co-authored-by: Felix Pernegger --- Mathlib/Algebra/Module/NatInt.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Algebra/Module/NatInt.lean b/Mathlib/Algebra/Module/NatInt.lean index 4d325e6b8c289d..67235bf345e303 100644 --- a/Mathlib/Algebra/Module/NatInt.lean +++ b/Mathlib/Algebra/Module/NatInt.lean @@ -5,7 +5,6 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro -/ module -public import Mathlib.Algebra.Group.Torsion public import Mathlib.Algebra.Module.Defs public import Mathlib.Data.Int.Cast.Lemmas