From 4bc7a2ce6b6d1e99fbbd99473a38c634c77bba39 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Tue, 10 Mar 2026 21:05:07 +0100 Subject: [PATCH 01/16] feat(Algebra/Group): some API lemmas for powMonoidHom --- Mathlib/Algebra/Group/Equiv/Basic.lean | 14 ++++++++++++++ Mathlib/Algebra/Group/Subgroup/Ker.lean | 18 ++++++++++++++++++ 2 files changed, 32 insertions(+) diff --git a/Mathlib/Algebra/Group/Equiv/Basic.lean b/Mathlib/Algebra/Group/Equiv/Basic.lean index 1a60aef1ddf2b4..8e39746bb50614 100644 --- a/Mathlib/Algebra/Group/Equiv/Basic.lean +++ b/Mathlib/Algebra/Group/Equiv/Basic.lean @@ -250,3 +250,17 @@ theorem inv_symm : (Equiv.inv G).symm = Equiv.inv G := rfl end InvolutiveInv end Equiv + +namespace MulEquiv + +variable [CommMonoid M] [CommMonoid N] + +/-- The `n`th power map commutes with isomorphisms. -/ +@[to_additive + /-- The multiplication-by-`n` map commutes with isomorphisms. -/] +lemma powMonoidHom_comm (e : M ≃* N) (n : ℕ) : + (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by + ext1 + simp + +end MulEquiv diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean index e7a4ee109334c2..5ab45ba05f971a 100644 --- a/Mathlib/Algebra/Group/Subgroup/Ker.lean +++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean @@ -8,6 +8,8 @@ module public import Mathlib.Algebra.Group.Subgroup.Map public import Mathlib.Tactic.ApplyFun +import Mathlib.Algebra.Group.Equiv.Basic + /-! # Kernel and range of group homomorphisms @@ -559,3 +561,19 @@ theorem codisjoint_subgroupOf_sup (H K : Subgroup G) : exacts [le_sup_left, le_sup_right] end Subgroup + +namespace MulEquiv + +@[to_additive] +lemma range_eq_top (e : G ≃* G') : (e : G →* G').range = ⊤ := + MonoidHom.range_eq_top.mpr e.surjective + +variable {M N : Type*} [CommGroup M] [CommGroup N] + +open MonoidHom in +@[to_additive] +lemma map_range_powMonoidHom (e : M ≃* N) (n : ℕ) : + (powMonoidHom (α := M) n).range.map e = (powMonoidHom (α := N) n).range := by + rw [map_range, e.powMonoidHom_comm, range_comp, e.range_eq_top, ← range_eq_map] + +end MulEquiv From 5b6f1f8b1671ea80826b9019cd3b83d9b1e57833 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Tue, 10 Mar 2026 22:12:35 +0100 Subject: [PATCH 02/16] add another lemma --- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean index b12177464e8006..c95d94daa23c13 100644 --- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean +++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean @@ -55,7 +55,17 @@ end Ring end AddSubgroup -@[simp] lemma Int.range_castAddHom {A : Type*} [AddGroupWithOne A] : +namespace Int + +@[simp] lemma range_castAddHom {A : Type*} [AddGroupWithOne A] : (Int.castAddHom A).range = AddSubgroup.zmultiples 1 := by ext a simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one] + +lemma range_nsmulAddMonoidHom (n : ℕ) : + (nsmulAddMonoidHom (α := ℤ) n).range = AddSubgroup.zmultiples (n : ℤ) := by + ext1 m + suffices (∃ x : ℤ , n * x = m) ↔ ∃ y, y * n = m by simpa only using this + refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩ <;> obtain ⟨k, rfl⟩ := H <;> exact ⟨k, Int.mul_comm ..⟩ + +end Int From 4699e882bc8721f2f9583ffe03d576b289c16b13 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Tue, 10 Mar 2026 22:14:52 +0100 Subject: [PATCH 03/16] open AddSubgroup, fix whitespace --- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean index c95d94daa23c13..ac0d2e1ece00f0 100644 --- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean +++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean @@ -57,15 +57,16 @@ end AddSubgroup namespace Int +open AddSubgroup + @[simp] lemma range_castAddHom {A : Type*} [AddGroupWithOne A] : - (Int.castAddHom A).range = AddSubgroup.zmultiples 1 := by + (castAddHom A).range = zmultiples 1 := by ext a simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one] -lemma range_nsmulAddMonoidHom (n : ℕ) : - (nsmulAddMonoidHom (α := ℤ) n).range = AddSubgroup.zmultiples (n : ℤ) := by +lemma range_nsmulAddMonoidHom (n : ℕ) : (nsmulAddMonoidHom n).range = zmultiples (n : ℤ) := by ext1 m - suffices (∃ x : ℤ , n * x = m) ↔ ∃ y, y * n = m by simpa only using this + suffices (∃ x : ℤ, n * x = m) ↔ ∃ y, y * n = m by simpa only using this refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩ <;> obtain ⟨k, rfl⟩ := H <;> exact ⟨k, Int.mul_comm ..⟩ end Int From a97b652098ae5c21bd79946bc720e608e4933f78 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 13:15:47 +0100 Subject: [PATCH 04/16] add def. of canonical iso. --- Mathlib/GroupTheory/QuotientGroup/Defs.lean | 22 +++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/Mathlib/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean index a827a7683beb55..013fde3523784e 100644 --- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean +++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean @@ -430,4 +430,26 @@ theorem congr_symm (e : G ≃* H) (he : G'.map ↑e = H') : end congr +section powMonoidHom + +/-- The isomorphism between the quotient of a product by the image of the `n`th power map +and the product of the quotients by the images of the `n`th power maps on the factors. -/ +@[to_additive + /-- The isomorphism between the quotient of a product by the image of the multiplication-by-`n` + map and the product of the quotients by the images of the multiplication-by-`n` maps + on the factors. -/ ] +noncomputable +def mulEquivPiModRangePowMonoidHom {ι : Type*} (A : ι → Type*) [∀ i, CommGroup (A i)] (n : ℕ) : + ((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range) := + let φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range := { + toFun x := (x ·) + map_one' := by simp [Pi.one_def] + map_mul' x y := by simp [Pi.mul_def] + } + liftEquiv (φ := φ) _ (fun y ↦ ⟨fun i ↦ Quotient.out (y i), by simp [φ]⟩) <| by + ext1 x + simpa [φ, funext_iff] using (Classical.skolem (p := fun i a ↦ a ^ n = x i)).symm + +end powMonoidHom + end QuotientGroup From 2724fe08419556302ff198f04a47b35e2291f681 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 17:53:43 +0100 Subject: [PATCH 05/16] add another powMonoidHom lemma --- Mathlib/Algebra/Group/Subgroup/Ker.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean index 5ab45ba05f971a..23b8b65f87788b 100644 --- a/Mathlib/Algebra/Group/Subgroup/Ker.lean +++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean @@ -560,6 +560,17 @@ theorem codisjoint_subgroupOf_sup (H K : Subgroup G) : rw [codisjoint_iff, ← subgroupOf_sup, subgroupOf_self] exacts [le_sup_left, le_sup_right] +variable {M : Type*} [CommGroup M] + +@[to_additive] +lemma subgroupOf_map_powMonoidHom_eq_range (S : Subgroup M) (n : ℕ) : + (map (powMonoidHom n) S).subgroupOf S = (powMonoidHom n).range := by + ext1 + simp only [mem_subgroupOf, mem_map, MonoidHom.mem_range, powMonoidHom_apply, Subtype.exists, + SubmonoidClass.mk_pow] + exact ⟨fun ⟨x, h₁, h₂⟩ ↦ ⟨x, h₁, Subtype.ext h₂⟩, + fun ⟨a, h₁, h₂⟩ ↦ ⟨a, h₁, Subtype.ext_iff.mp h₂⟩⟩ + end Subgroup namespace MulEquiv From d5a5426734fd0b03c7a75dc6008e2b7c0956dd20 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 20:18:42 +0100 Subject: [PATCH 06/16] feat(GroupTheory/IndexNSmul): new file --- Mathlib/GroupTheory/IndexNSmul.lean | 99 +++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 Mathlib/GroupTheory/IndexNSmul.lean diff --git a/Mathlib/GroupTheory/IndexNSmul.lean b/Mathlib/GroupTheory/IndexNSmul.lean new file mode 100644 index 00000000000000..2f66892abae7d9 --- /dev/null +++ b/Mathlib/GroupTheory/IndexNSmul.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Michael Stoll. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Stoll +-/ +module + +public import Mathlib.GroupTheory.Index +public import Mathlib.LinearAlgebra.Dimension.Finrank +public import Mathlib.LinearAlgebra.FreeModule.Basic +public import Mathlib.RingTheory.Finiteness.Defs + +import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas +import Mathlib.Data.ZMod.QuotientGroup +import Mathlib.LinearAlgebra.Dimension.Constructions +import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition + +/-! +# Lemmas about index and multiplication-by-n + +In this file we collect some results involving the multiplication-by-`n` map +`nsmulAddMonoidHom n` (for a natural number `n`) on a commutative additive group +and the (relative) index of subgroups. +-/ + +public section + +namespace AddSubgroup + +variable {M N : Type*} [AddCommGroup M] [AddCommGroup N] + +open Module + +open QuotientAddGroup in +variable (M) in +/-- The index of the image of the multiplication-by-`n` map on an additive group `M` that is free +and finitely generated as a `ℤ`-module is `n ^ finrank ℤ M`. -/ +lemma index_nsmul [Free ℤ M] [Module.Finite ℤ M] (n : ℕ) : + (nsmulAddMonoidHom (α := M) n).range.index = n ^ finrank ℤ M := by + let e := (Module.finBasis ℤ M).equivFun + suffices (nsmulAddMonoidHom (α := Fin (finrank ℤ M) → ℤ) n).range.index = n ^ finrank ℤ M by + rwa [← AddEquiv.map_range_nsmulAddMonoidHom e.toAddEquiv, index_map_equiv] at this + simp [index_eq_card, Nat.card_congr (addEquivPiModRangeNSMulAddMonoidHom _ n).toEquiv, + Nat.card_fun, Int.range_nsmulAddMonoidHom, + Nat.card_congr (Int.quotientZMultiplesNatEquivZMod n).toEquiv] + +/-- The relative index in `S` of the image of the multiplication-by-`n` map +on an additive subgroup `S` of an additive group such that `S` is free +and finitely generated as a `ℤ`-module is `n ^ finrank ℤ S`. -/ +lemma relIndex_nsmul (n : ℕ) (S : AddSubgroup M) [Free ℤ ↥S.toIntSubmodule] + [Module.Finite ℤ ↥S.toIntSubmodule] : + (S.map (nsmulAddMonoidHom (α := M) n)).relIndex S = n ^ finrank ℤ S := by + simpa only [relIndex, addSubgroupOf_map_nsmulAddMonoidHom_eq_range] + using index_nsmul S.toIntSubmodule n + +/-- On an additive group that is torsion-free as a `ℤ`-module, the linear map given by +multiplication by `n : ℕ` is injective (when `n ≠ 0`). -/ +lemma distribSMulToLinearMap_injective_of_isTorsionFree [IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : + Function.Injective (DistribSMul.toLinearMap ℤ M n) := by + refine LinearMap.ker_eq_bot.mp <| (Submodule.eq_bot_iff _).mpr fun x hx ↦ ?_ + simp only [LinearMap.mem_ker, DistribSMul.toLinearMap_apply, ← natCast_zsmul] at hx + exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx + +/-- On an additive group that is torsion-free as a `ℤ`-module, the multiplication-by-`n` map +is injective (when `n ≠ 0`). -/ +lemma nsmulAddMonoidHom_injective_of_isTorsionFree [IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : + Function.Injective (nsmulAddMonoidHom (α := M) n) := by + refine (AddMonoidHom.ker_eq_bot_iff _).mp <| (eq_bot_iff_forall _).mpr fun x hx ↦ ?_ + simp only [AddMonoidHom.mem_ker, nsmulAddMonoidHom_apply, ← natCast_zsmul] at hx + exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx + +/-- If `A` is a subgroup of finite index of an additive group `M` that is finitely generated +and torsion-free as a `ℤ`-module, then `A` and `M` have the same rank. -/ +lemma finrank_eq_of_finiteIndex [Module.Finite ℤ M] [IsTorsionFree ℤ M] (A : AddSubgroup M) + [A.FiniteIndex] : + finrank ℤ A = finrank ℤ M := by + refine le_antisymm ?_ ?_ + · rw [← finrank_top ℤ M] + exact Submodule.finrank_mono (s := A.toIntSubmodule) le_top + · set n := A.index + rw [← (DistribSMul.toLinearMap ℤ M n).finrank_range_of_inj <| + distribSMulToLinearMap_injective_of_isTorsionFree FiniteIndex.index_ne_zero] + refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_ + obtain ⟨x, rfl⟩ : ∃ x, n • x = m := by simpa using hm + exact A.nsmul_index_mem x + +/-- If `A ≤ B` are subgroups of an additive group `M` such that `A` has finite relative index +in `B`, where `B` is finitely generated and torsion-free as a `ℤ`-module, then `A` and `B` +have the same rank. -/ +lemma finrank_eq_of_isFiniteRelIndex {A B : AddSubgroup M} [Module.Finite ℤ B] [IsTorsionFree ℤ B] + (h : A ≤ B) [A.IsFiniteRelIndex B] : + finrank ℤ A = finrank ℤ B := by + have : (A.addSubgroupOf B).FiniteIndex := IsFiniteRelIndex.to_finiteIndex_addSubgroupOf + rw [← finrank_eq_of_finiteIndex (A.addSubgroupOf B)] + exact (addSubgroupOfEquivOfLe h).symm.toIntLinearEquiv.finrank_eq + +end AddSubgroup + +end From 9bad6f90a0a8ebe344505b18a9d3a23bc1ed35e8 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 20:27:44 +0100 Subject: [PATCH 07/16] move mulEquivPiModRangePowMonoidHom --- Mathlib/GroupTheory/QuotientGroup/Basic.lean | 26 ++++++++++++++++++++ Mathlib/GroupTheory/QuotientGroup/Defs.lean | 22 ----------------- 2 files changed, 26 insertions(+), 22 deletions(-) diff --git a/Mathlib/GroupTheory/QuotientGroup/Basic.lean b/Mathlib/GroupTheory/QuotientGroup/Basic.lean index b4138fefcf4d96..a0f4fb45e09b0e 100644 --- a/Mathlib/GroupTheory/QuotientGroup/Basic.lean +++ b/Mathlib/GroupTheory/QuotientGroup/Basic.lean @@ -441,3 +441,29 @@ theorem mk_int_mul (n : ℤ) (a : R) : ((n * a : R) : R ⧸ N) = n • ↑a := b rw [← zsmul_eq_mul, mk_zsmul N a n] end QuotientAddGroup + +namespace QuotientGroup + +section powMonoidHom + +/-- The isomorphism between the quotient of a product by the image of the `n`th power map +and the product of the quotients by the images of the `n`th power maps on the factors. -/ +@[to_additive + /-- The isomorphism between the quotient of a product by the image of the multiplication-by-`n` + map and the product of the quotients by the images of the multiplication-by-`n` maps + on the factors. -/ ] +noncomputable +def mulEquivPiModRangePowMonoidHom {ι : Type*} (A : ι → Type*) [∀ i, CommGroup (A i)] (n : ℕ) : + ((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range) := + let φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range := { + toFun x := (x ·) + map_one' := by simp [Pi.one_def] + map_mul' x y := by simp [Pi.mul_def] + } + liftEquiv (φ := φ) _ (fun y ↦ ⟨fun i ↦ Quotient.out (y i), by simp [φ]⟩) <| by + ext1 x + simpa [φ, funext_iff] using (Classical.skolem (p := fun i a ↦ a ^ n = x i)).symm + +end powMonoidHom + +end QuotientGroup diff --git a/Mathlib/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean index 013fde3523784e..a827a7683beb55 100644 --- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean +++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean @@ -430,26 +430,4 @@ theorem congr_symm (e : G ≃* H) (he : G'.map ↑e = H') : end congr -section powMonoidHom - -/-- The isomorphism between the quotient of a product by the image of the `n`th power map -and the product of the quotients by the images of the `n`th power maps on the factors. -/ -@[to_additive - /-- The isomorphism between the quotient of a product by the image of the multiplication-by-`n` - map and the product of the quotients by the images of the multiplication-by-`n` maps - on the factors. -/ ] -noncomputable -def mulEquivPiModRangePowMonoidHom {ι : Type*} (A : ι → Type*) [∀ i, CommGroup (A i)] (n : ℕ) : - ((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range) := - let φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range := { - toFun x := (x ·) - map_one' := by simp [Pi.one_def] - map_mul' x y := by simp [Pi.mul_def] - } - liftEquiv (φ := φ) _ (fun y ↦ ⟨fun i ↦ Quotient.out (y i), by simp [φ]⟩) <| by - ext1 x - simpa [φ, funext_iff] using (Classical.skolem (p := fun i a ↦ a ^ n = x i)).symm - -end powMonoidHom - end QuotientGroup From 8d9c380c732d7973ae55cd828bf7b614c8418eb3 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 20:31:13 +0100 Subject: [PATCH 08/16] remove powMonoidHom_comm, inline at use site --- Mathlib/Algebra/Group/Equiv/Basic.lean | 14 -------------- Mathlib/Algebra/Group/Subgroup/Ker.lean | 3 ++- 2 files changed, 2 insertions(+), 15 deletions(-) diff --git a/Mathlib/Algebra/Group/Equiv/Basic.lean b/Mathlib/Algebra/Group/Equiv/Basic.lean index 8e39746bb50614..1a60aef1ddf2b4 100644 --- a/Mathlib/Algebra/Group/Equiv/Basic.lean +++ b/Mathlib/Algebra/Group/Equiv/Basic.lean @@ -250,17 +250,3 @@ theorem inv_symm : (Equiv.inv G).symm = Equiv.inv G := rfl end InvolutiveInv end Equiv - -namespace MulEquiv - -variable [CommMonoid M] [CommMonoid N] - -/-- The `n`th power map commutes with isomorphisms. -/ -@[to_additive - /-- The multiplication-by-`n` map commutes with isomorphisms. -/] -lemma powMonoidHom_comm (e : M ≃* N) (n : ℕ) : - (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by - ext1 - simp - -end MulEquiv diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean index 23b8b65f87788b..835e5e49281a0f 100644 --- a/Mathlib/Algebra/Group/Subgroup/Ker.lean +++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean @@ -585,6 +585,7 @@ open MonoidHom in @[to_additive] lemma map_range_powMonoidHom (e : M ≃* N) (n : ℕ) : (powMonoidHom (α := M) n).range.map e = (powMonoidHom (α := N) n).range := by - rw [map_range, e.powMonoidHom_comm, range_comp, e.range_eq_top, ← range_eq_map] + have H : (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by ext; simp + rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map] end MulEquiv From df16bef8b7178bae7bfa69c4e13ea24d35cf4c64 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 20:34:26 +0100 Subject: [PATCH 09/16] golf following review suggestions --- Mathlib/Algebra/Group/Subgroup/Ker.lean | 8 +++----- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean | 4 ++-- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean index 835e5e49281a0f..cce378d5173699 100644 --- a/Mathlib/Algebra/Group/Subgroup/Ker.lean +++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean @@ -565,11 +565,9 @@ variable {M : Type*} [CommGroup M] @[to_additive] lemma subgroupOf_map_powMonoidHom_eq_range (S : Subgroup M) (n : ℕ) : (map (powMonoidHom n) S).subgroupOf S = (powMonoidHom n).range := by - ext1 - simp only [mem_subgroupOf, mem_map, MonoidHom.mem_range, powMonoidHom_apply, Subtype.exists, - SubmonoidClass.mk_pow] - exact ⟨fun ⟨x, h₁, h₂⟩ ↦ ⟨x, h₁, Subtype.ext h₂⟩, - fun ⟨a, h₁, h₂⟩ ↦ ⟨a, h₁, Subtype.ext_iff.mp h₂⟩⟩ + ext + simp [mem_subgroupOf] + grind end Subgroup diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean index ac0d2e1ece00f0..23345d1c1c782b 100644 --- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean +++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean @@ -66,7 +66,7 @@ open AddSubgroup lemma range_nsmulAddMonoidHom (n : ℕ) : (nsmulAddMonoidHom n).range = zmultiples (n : ℤ) := by ext1 m - suffices (∃ x : ℤ, n * x = m) ↔ ∃ y, y * n = m by simpa only using this - refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩ <;> obtain ⟨k, rfl⟩ := H <;> exact ⟨k, Int.mul_comm ..⟩ + simp [mem_zmultiples_iff, dvd_def] + grind end Int From a8cb224098ea7398fb62df5b6649164fa6ee5037 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 20:35:29 +0100 Subject: [PATCH 10/16] add 'simp' attribuite --- Mathlib/Algebra/Group/Subgroup/Ker.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean index cce378d5173699..e80671d43776ad 100644 --- a/Mathlib/Algebra/Group/Subgroup/Ker.lean +++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean @@ -573,7 +573,7 @@ end Subgroup namespace MulEquiv -@[to_additive] +@[to_additive (attr := simp)] lemma range_eq_top (e : G ≃* G') : (e : G →* G').range = ⊤ := MonoidHom.range_eq_top.mpr e.surjective From 5a6f810a9ea564c6b6ab2b8f9b9a4dd4d0475ca1 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 11 Mar 2026 20:38:43 +0100 Subject: [PATCH 11/16] run mk_all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index e96985d0ef81e6..57d98a5cbfa0ce 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4535,6 +4535,7 @@ public import Mathlib.GroupTheory.GroupExtension.Basic public import Mathlib.GroupTheory.GroupExtension.Defs public import Mathlib.GroupTheory.HNNExtension public import Mathlib.GroupTheory.Index +public import Mathlib.GroupTheory.IndexNSmul public import Mathlib.GroupTheory.IndexNormal public import Mathlib.GroupTheory.IsPerfect public import Mathlib.GroupTheory.IsSubnormal From 65b7c62b719115f1a55736c0fb28fb75cedc5488 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Thu, 26 Mar 2026 19:49:05 +0100 Subject: [PATCH 12/16] remove double import --- Mathlib/Algebra/Group/Subgroup/Ker.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean index 982205493ede43..752cf3f7138cea 100644 --- a/Mathlib/Algebra/Group/Subgroup/Ker.lean +++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean @@ -10,8 +10,6 @@ public import Mathlib.Tactic.ApplyFun import Mathlib.Algebra.Group.Equiv.Basic -import Mathlib.Algebra.Group.Equiv.Basic - /-! # Kernel and range of group homomorphisms From 501be151f99ea7926dc1996c1f69ac71451e2279 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Thu, 26 Mar 2026 19:50:57 +0100 Subject: [PATCH 13/16] fix indentation --- Mathlib/GroupTheory/IndexNSmul.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/GroupTheory/IndexNSmul.lean b/Mathlib/GroupTheory/IndexNSmul.lean index 2f66892abae7d9..713a349dd2eba1 100644 --- a/Mathlib/GroupTheory/IndexNSmul.lean +++ b/Mathlib/GroupTheory/IndexNSmul.lean @@ -57,17 +57,17 @@ lemma relIndex_nsmul (n : ℕ) (S : AddSubgroup M) [Free ℤ ↥S.toIntSubmodule multiplication by `n : ℕ` is injective (when `n ≠ 0`). -/ lemma distribSMulToLinearMap_injective_of_isTorsionFree [IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : Function.Injective (DistribSMul.toLinearMap ℤ M n) := by - refine LinearMap.ker_eq_bot.mp <| (Submodule.eq_bot_iff _).mpr fun x hx ↦ ?_ - simp only [LinearMap.mem_ker, DistribSMul.toLinearMap_apply, ← natCast_zsmul] at hx - exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx + refine LinearMap.ker_eq_bot.mp <| (Submodule.eq_bot_iff _).mpr fun x hx ↦ ?_ + simp only [LinearMap.mem_ker, DistribSMul.toLinearMap_apply, ← natCast_zsmul] at hx + exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx /-- On an additive group that is torsion-free as a `ℤ`-module, the multiplication-by-`n` map is injective (when `n ≠ 0`). -/ lemma nsmulAddMonoidHom_injective_of_isTorsionFree [IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : Function.Injective (nsmulAddMonoidHom (α := M) n) := by - refine (AddMonoidHom.ker_eq_bot_iff _).mp <| (eq_bot_iff_forall _).mpr fun x hx ↦ ?_ - simp only [AddMonoidHom.mem_ker, nsmulAddMonoidHom_apply, ← natCast_zsmul] at hx - exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx + refine (AddMonoidHom.ker_eq_bot_iff _).mp <| (eq_bot_iff_forall _).mpr fun x hx ↦ ?_ + simp only [AddMonoidHom.mem_ker, nsmulAddMonoidHom_apply, ← natCast_zsmul] at hx + exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx /-- If `A` is a subgroup of finite index of an additive group `M` that is finitely generated and torsion-free as a `ℤ`-module, then `A` and `M` have the same rank. -/ From 204948221e55851c500e6cfd9fd89ab1ebee1ae5 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Thu, 26 Mar 2026 20:01:11 +0100 Subject: [PATCH 14/16] fix garbled file --- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean index cdc5f735cdb304..1b833db2404749 100644 --- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean +++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean @@ -59,12 +59,6 @@ namespace Int open AddSubgroup -@[simp] lemma range_castAddHom {A : Type*} [AddGroupWithOne A] : - (castAddHom A).range = zmultiples 1 := by -namespace Int - -open AddSubgroup - @[simp] lemma range_castAddHom {A : Type*} [AddGroupWithOne A] : (castAddHom A).range = zmultiples 1 := by ext a From 62496c9a0f20e4c69f3682be575e645cfa2d36e5 Mon Sep 17 00:00:00 2001 From: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> Date: Thu, 2 Apr 2026 22:43:42 +0200 Subject: [PATCH 15/16] Apply suggestions from code review Co-authored-by: Dagur Asgeirsson --- Mathlib/GroupTheory/IndexNSmul.lean | 32 +++++++++++------------------ 1 file changed, 12 insertions(+), 20 deletions(-) diff --git a/Mathlib/GroupTheory/IndexNSmul.lean b/Mathlib/GroupTheory/IndexNSmul.lean index 713a349dd2eba1..451cbb65b29969 100644 --- a/Mathlib/GroupTheory/IndexNSmul.lean +++ b/Mathlib/GroupTheory/IndexNSmul.lean @@ -37,9 +37,8 @@ variable (M) in and finitely generated as a `ℤ`-module is `n ^ finrank ℤ M`. -/ lemma index_nsmul [Free ℤ M] [Module.Finite ℤ M] (n : ℕ) : (nsmulAddMonoidHom (α := M) n).range.index = n ^ finrank ℤ M := by - let e := (Module.finBasis ℤ M).equivFun - suffices (nsmulAddMonoidHom (α := Fin (finrank ℤ M) → ℤ) n).range.index = n ^ finrank ℤ M by - rwa [← AddEquiv.map_range_nsmulAddMonoidHom e.toAddEquiv, index_map_equiv] at this + rw [← index_map_equiv _ (Module.finBasis ℤ M).equivFun.toAddEquiv, + AddEquiv.map_range_nsmulAddMonoidHom] simp [index_eq_card, Nat.card_congr (addEquivPiModRangeNSMulAddMonoidHom _ n).toEquiv, Nat.card_fun, Int.range_nsmulAddMonoidHom, Nat.card_congr (Int.quotientZMultiplesNatEquivZMod n).toEquiv] @@ -56,33 +55,26 @@ lemma relIndex_nsmul (n : ℕ) (S : AddSubgroup M) [Free ℤ ↥S.toIntSubmodule /-- On an additive group that is torsion-free as a `ℤ`-module, the linear map given by multiplication by `n : ℕ` is injective (when `n ≠ 0`). -/ lemma distribSMulToLinearMap_injective_of_isTorsionFree [IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : - Function.Injective (DistribSMul.toLinearMap ℤ M n) := by - refine LinearMap.ker_eq_bot.mp <| (Submodule.eq_bot_iff _).mpr fun x hx ↦ ?_ - simp only [LinearMap.mem_ker, DistribSMul.toLinearMap_apply, ← natCast_zsmul] at hx - exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx + Function.Injective (DistribSMul.toLinearMap ℤ M n) := + LinearMap.ker_eq_bot.mp <| (Submodule.eq_bot_iff _).mpr fun x hx ↦ by simp_all /-- On an additive group that is torsion-free as a `ℤ`-module, the multiplication-by-`n` map is injective (when `n ≠ 0`). -/ lemma nsmulAddMonoidHom_injective_of_isTorsionFree [IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : - Function.Injective (nsmulAddMonoidHom (α := M) n) := by - refine (AddMonoidHom.ker_eq_bot_iff _).mp <| (eq_bot_iff_forall _).mpr fun x hx ↦ ?_ - simp only [AddMonoidHom.mem_ker, nsmulAddMonoidHom_apply, ← natCast_zsmul] at hx - exact (smul_eq_zero_iff_right <| mod_cast hn).mp hx + Function.Injective (nsmulAddMonoidHom (α := M) n) := + (AddMonoidHom.ker_eq_bot_iff _).mp <| (eq_bot_iff_forall _).mpr fun x hx ↦ by simp_all /-- If `A` is a subgroup of finite index of an additive group `M` that is finitely generated and torsion-free as a `ℤ`-module, then `A` and `M` have the same rank. -/ lemma finrank_eq_of_finiteIndex [Module.Finite ℤ M] [IsTorsionFree ℤ M] (A : AddSubgroup M) [A.FiniteIndex] : finrank ℤ A = finrank ℤ M := by - refine le_antisymm ?_ ?_ - · rw [← finrank_top ℤ M] - exact Submodule.finrank_mono (s := A.toIntSubmodule) le_top - · set n := A.index - rw [← (DistribSMul.toLinearMap ℤ M n).finrank_range_of_inj <| - distribSMulToLinearMap_injective_of_isTorsionFree FiniteIndex.index_ne_zero] - refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_ - obtain ⟨x, rfl⟩ : ∃ x, n • x = m := by simpa using hm - exact A.nsmul_index_mem x + refine le_antisymm A.toIntSubmodule.finrank_le ?_ + rw [← (DistribSMul.toLinearMap ℤ M A.index).finrank_range_of_inj <| + distribSMulToLinearMap_injective_of_isTorsionFree FiniteIndex.index_ne_zero] + refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_ + obtain ⟨x, rfl⟩ : ∃ x, A.index • x = m := by simpa using hm + exact A.nsmul_index_mem x /-- If `A ≤ B` are subgroups of an additive group `M` such that `A` has finite relative index in `B`, where `B` is finitely generated and torsion-free as a `ℤ`-module, then `A` and `B` From dc5730d2dc4e6a73453d91cb7d1fcdb4a03ab2ab Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Thu, 9 Apr 2026 21:42:06 +0200 Subject: [PATCH 16/16] suggestions from review --- Mathlib/GroupTheory/IndexNSmul.lean | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/Mathlib/GroupTheory/IndexNSmul.lean b/Mathlib/GroupTheory/IndexNSmul.lean index 451cbb65b29969..c3e5b08c03a741 100644 --- a/Mathlib/GroupTheory/IndexNSmul.lean +++ b/Mathlib/GroupTheory/IndexNSmul.lean @@ -35,22 +35,26 @@ open QuotientAddGroup in variable (M) in /-- The index of the image of the multiplication-by-`n` map on an additive group `M` that is free and finitely generated as a `ℤ`-module is `n ^ finrank ℤ M`. -/ -lemma index_nsmul [Free ℤ M] [Module.Finite ℤ M] (n : ℕ) : - (nsmulAddMonoidHom (α := M) n).range.index = n ^ finrank ℤ M := by - rw [← index_map_equiv _ (Module.finBasis ℤ M).equivFun.toAddEquiv, - AddEquiv.map_range_nsmulAddMonoidHom] - simp [index_eq_card, Nat.card_congr (addEquivPiModRangeNSMulAddMonoidHom _ n).toEquiv, - Nat.card_fun, Int.range_nsmulAddMonoidHom, - Nat.card_congr (Int.quotientZMultiplesNatEquivZMod n).toEquiv] +lemma index_range_nsmul [Free ℤ M] [Module.Finite ℤ M] (n : ℕ) : + (nsmulAddMonoidHom (α := M) n).range.index = n ^ finrank ℤ M := + calc + _ = (nsmulAddMonoidHom (α := (Fin (finrank ℤ M) → ℤ)) n).range.index := by + simpa [AddEquiv.map_range_nsmulAddMonoidHom] + using (index_map_equiv (nsmulAddMonoidHom (α := M) n).range + (Module.finBasis ℤ M).equivFun.toAddEquiv).symm + _ = _ := by + simp [index_eq_card, Nat.card_congr (addEquivPiModRangeNSMulAddMonoidHom _ n).toEquiv, + Nat.card_fun, Int.range_nsmulAddMonoidHom, + Nat.card_congr (Int.quotientZMultiplesNatEquivZMod n).toEquiv] /-- The relative index in `S` of the image of the multiplication-by-`n` map on an additive subgroup `S` of an additive group such that `S` is free and finitely generated as a `ℤ`-module is `n ^ finrank ℤ S`. -/ -lemma relIndex_nsmul (n : ℕ) (S : AddSubgroup M) [Free ℤ ↥S.toIntSubmodule] +lemma relIndex_map_nsmul (n : ℕ) (S : AddSubgroup M) [Free ℤ ↥S.toIntSubmodule] [Module.Finite ℤ ↥S.toIntSubmodule] : (S.map (nsmulAddMonoidHom (α := M) n)).relIndex S = n ^ finrank ℤ S := by simpa only [relIndex, addSubgroupOf_map_nsmulAddMonoidHom_eq_range] - using index_nsmul S.toIntSubmodule n + using index_range_nsmul S.toIntSubmodule n /-- On an additive group that is torsion-free as a `ℤ`-module, the linear map given by multiplication by `n : ℕ` is injective (when `n ≠ 0`). -/ @@ -70,8 +74,10 @@ lemma finrank_eq_of_finiteIndex [Module.Finite ℤ M] [IsTorsionFree ℤ M] (A : [A.FiniteIndex] : finrank ℤ A = finrank ℤ M := by refine le_antisymm A.toIntSubmodule.finrank_le ?_ - rw [← (DistribSMul.toLinearMap ℤ M A.index).finrank_range_of_inj <| - distribSMulToLinearMap_injective_of_isTorsionFree FiniteIndex.index_ne_zero] + have : finrank ℤ (DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M := + (DistribSMul.toLinearMap ..).finrank_range_of_inj <| + distribSMulToLinearMap_injective_of_isTorsionFree FiniteIndex.index_ne_zero + rw [← this] refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_ obtain ⟨x, rfl⟩ : ∃ x, A.index • x = m := by simpa using hm exact A.nsmul_index_mem x