From 578b842ca62b225655e4b0899a4ed934431d2bf9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Sun, 28 Jan 2024 21:20:55 -0500 Subject: [PATCH 1/5] move the lemma --- Mathlib/GroupTheory/Index.lean | 23 +++++++++++++++++++++++ Mathlib/RingTheory/IntegralDomain.lean | 23 +---------------------- 2 files changed, 24 insertions(+), 22 deletions(-) diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean index 042746dbf460fc..afed21ac4c9a07 100644 --- a/Mathlib/GroupTheory/Index.lean +++ b/Mathlib/GroupTheory/Index.lean @@ -614,3 +614,26 @@ theorem index_center_le_pow [Finite (commutatorSet G)] [Group.FG G] : end FiniteIndex end Subgroup + +namespace MonoidHom + +variable {G H F : Type*} [Group G] [Fintype G] [Group H] [DecidableEq H] [MonoidHomClass F G H] + +open Finset in +@[to_additive] +theorem card_fiber_eq_of_mem_range (f : F) {x y : H} (hx : x ∈ Set.range f) + (hy : y ∈ Set.range f) : + -- porting note: the `filter` had an index `ₓ` that I removed. + (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by + rcases hx with ⟨x, rfl⟩ + rcases hy with ⟨y, rfl⟩ + refine card_congr (fun g _ => g * x⁻¹ * y) ?_ ?_ fun g hg => ⟨g * y⁻¹ * x, ?_⟩ + · simp (config := { contextual := true }) only [mem_filter, mem_univ, true_and, map_mul, map_inv, + mul_right_inv, one_mul, and_self, implies_true, forall_const] + · simp only [mul_left_inj, imp_self, forall₂_true_iff] + · simp only [true_and_iff, mem_filter, mem_univ] at hg + simp only [mul_inv_cancel_right, inv_mul_cancel_right, mem_filter, mem_univ, map_mul, hg, + map_inv, mul_right_inv, one_mul, and_self, exists_prop_of_true] +#align card_fiber_eq_of_mem_range MonoidHom.card_fiber_eq_of_mem_range + +end MonoidHom diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean index 5eb43c6b4eca09..76093e0ed5a0fa 100644 --- a/Mathlib/RingTheory/IntegralDomain.lean +++ b/Mathlib/RingTheory/IntegralDomain.lean @@ -189,27 +189,6 @@ end EuclideanDivision variable [Fintype G] -theorem card_fiber_eq_of_mem_range {H : Type*} [Group H] [DecidableEq H] (f : G →* H) {x y : H} - (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) : - -- porting note: the `filter` had an index `ₓ` that I removed. - (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by - rcases hx with ⟨x, rfl⟩ - rcases hy with ⟨y, rfl⟩ - refine' card_congr (fun g _ => g * x⁻¹ * y) _ _ fun g hg => ⟨g * y⁻¹ * x, _⟩ - · simp (config := { contextual := true }) only [*, mem_filter, one_mul, MonoidHom.map_mul, - mem_univ, mul_right_inv, eq_self_iff_true, MonoidHom.map_mul_inv, and_self_iff, - forall_true_iff] - -- porting note: added the following `simp` - simp only [true_and, map_inv, mul_right_inv, one_mul, and_self, implies_true, forall_const] - · simp only [mul_left_inj, imp_self, forall₂_true_iff] - · simp only [true_and_iff, mem_filter, mem_univ] at hg - simp only [hg, mem_filter, one_mul, MonoidHom.map_mul, mem_univ, mul_right_inv, - eq_self_iff_true, exists_prop_of_true, MonoidHom.map_mul_inv, and_self_iff, - mul_inv_cancel_right, inv_mul_cancel_right] - -- porting note: added the next line. It is weird! - simp only [map_inv, mul_right_inv, one_mul, and_self, exists_prop] -#align card_fiber_eq_of_mem_range card_fiber_eq_of_mem_range - /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero. -/ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 := by @@ -246,7 +225,7 @@ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 _ = (0 : R) := smul_zero _ · -- remaining goal 1 show (univ.filter fun g : G => f.toHomUnits g = u).card = c - apply card_fiber_eq_of_mem_range f.toHomUnits + apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits · simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu · exact ⟨1, f.toHomUnits.map_one⟩ -- remaining goal 2 From d76ed0c64ecccdf90d386a971c8ac16b97681266 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Sun, 28 Jan 2024 21:36:02 -0500 Subject: [PATCH 2/5] split lemma --- Mathlib/GroupTheory/Index.lean | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean index afed21ac4c9a07..369a141189bf13 100644 --- a/Mathlib/GroupTheory/Index.lean +++ b/Mathlib/GroupTheory/Index.lean @@ -617,23 +617,27 @@ end Subgroup namespace MonoidHom +open Finset + variable {G H F : Type*} [Group G] [Fintype G] [Group H] [DecidableEq H] [MonoidHomClass F G H] -open Finset in @[to_additive] -theorem card_fiber_eq_of_mem_range (f : F) {x y : H} (hx : x ∈ Set.range f) - (hy : y ∈ Set.range f) : - -- porting note: the `filter` had an index `ₓ` that I removed. - (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by +theorem card_fiber_of_mem_range (f : F) {x : H} (hx : x ∈ Set.range f) : + (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = 1).card := by rcases hx with ⟨x, rfl⟩ - rcases hy with ⟨y, rfl⟩ - refine card_congr (fun g _ => g * x⁻¹ * y) ?_ ?_ fun g hg => ⟨g * y⁻¹ * x, ?_⟩ - · simp (config := { contextual := true }) only [mem_filter, mem_univ, true_and, map_mul, map_inv, - mul_right_inv, one_mul, and_self, implies_true, forall_const] + refine card_congr (fun g _ => g * x⁻¹ * 1) ?_ ?_ fun g hg => ⟨g * 1⁻¹ * x, ?_⟩ + · simp (config := { contextual := true }) only [mem_filter, mem_univ, true_and, mul_one, map_mul, + map_inv, mul_right_inv, and_self, implies_true, forall_const] · simp only [mul_left_inj, imp_self, forall₂_true_iff] · simp only [true_and_iff, mem_filter, mem_univ] at hg - simp only [mul_inv_cancel_right, inv_mul_cancel_right, mem_filter, mem_univ, map_mul, hg, - map_inv, mul_right_inv, one_mul, and_self, exists_prop_of_true] + simp only [inv_one, mul_one, mul_inv_cancel_right, mem_filter, mem_univ, map_mul, hg, one_mul, + and_self, exists_prop_of_true] + +@[to_additive] +theorem card_fiber_eq_of_mem_range (f : F) {x y : H} (hx : x ∈ Set.range f) + (hy : y ∈ Set.range f) : + (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by + simp only [card_fiber_of_mem_range f hx, card_fiber_of_mem_range f hy] #align card_fiber_eq_of_mem_range MonoidHom.card_fiber_eq_of_mem_range end MonoidHom From 967a22f07a5c07872683b548b4d58169d56e3d3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Sun, 9 Jun 2024 20:54:07 -0400 Subject: [PATCH 3/5] bump to modern master --- Mathlib/GroupTheory/Index.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean index 4b37e8b20de851..e4da5783222e26 100644 --- a/Mathlib/GroupTheory/Index.lean +++ b/Mathlib/GroupTheory/Index.lean @@ -620,13 +620,14 @@ namespace MonoidHom open Finset -variable {G H F : Type*} [Group G] [Fintype G] [Group H] [DecidableEq H] [MonoidHomClass F G H] +variable {G H F : Type*} [Group G] [Fintype G] [Group H] [DecidableEq H] + [FunLike F G H] [MonoidHomClass F G H] @[to_additive] theorem card_fiber_of_mem_range (f : F) {x : H} (hx : x ∈ Set.range f) : (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = 1).card := by rcases hx with ⟨x, rfl⟩ - refine card_congr (fun g _ => g * x⁻¹ * 1) ?_ ?_ fun g hg => ⟨g * 1⁻¹ * x, ?_⟩ + refine card_bij (fun g _ => g * x⁻¹ * 1) ?_ ?_ fun g hg => ⟨g * 1⁻¹ * x, ?_⟩ · simp (config := { contextual := true }) only [mem_filter, mem_univ, true_and, mul_one, map_mul, map_inv, mul_right_inv, and_self, implies_true, forall_const] · simp only [mul_left_inj, imp_self, forall₂_true_iff] From e54a6bb21c368c6f321735afda1d49095954e508 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Sun, 9 Jun 2024 21:09:19 -0400 Subject: [PATCH 4/5] use Yury's generalization + proof --- Mathlib/GroupTheory/Index.lean | 31 +++++++++++++------------------ 1 file changed, 13 insertions(+), 18 deletions(-) diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean index e4da5783222e26..c8e29161e5566c 100644 --- a/Mathlib/GroupTheory/Index.lean +++ b/Mathlib/GroupTheory/Index.lean @@ -620,26 +620,21 @@ namespace MonoidHom open Finset -variable {G H F : Type*} [Group G] [Fintype G] [Group H] [DecidableEq H] - [FunLike F G H] [MonoidHomClass F G H] +variable {G M F : Type*} [Group G] [Fintype G] [Monoid M] [DecidableEq M] + [FunLike F G M] [MonoidHomClass F G M] @[to_additive] -theorem card_fiber_of_mem_range (f : F) {x : H} (hx : x ∈ Set.range f) : - (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = 1).card := by +lemma card_fiber_eq_of_mem_range (f : F) {x y : M} (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) : + (univ.filter <| fun g => f g = x).card = (univ.filter <| fun g => f g = y).card := by rcases hx with ⟨x, rfl⟩ - refine card_bij (fun g _ => g * x⁻¹ * 1) ?_ ?_ fun g hg => ⟨g * 1⁻¹ * x, ?_⟩ - · simp (config := { contextual := true }) only [mem_filter, mem_univ, true_and, mul_one, map_mul, - map_inv, mul_right_inv, and_self, implies_true, forall_const] - · simp only [mul_left_inj, imp_self, forall₂_true_iff] - · simp only [true_and_iff, mem_filter, mem_univ] at hg - simp only [inv_one, mul_one, mul_inv_cancel_right, mem_filter, mem_univ, map_mul, hg, one_mul, - and_self, exists_prop_of_true] - -@[to_additive] -theorem card_fiber_eq_of_mem_range (f : F) {x y : H} (hx : x ∈ Set.range f) - (hy : y ∈ Set.range f) : - (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by - simp only [card_fiber_of_mem_range f hx, card_fiber_of_mem_range f hy] -#align card_fiber_eq_of_mem_range MonoidHom.card_fiber_eq_of_mem_range + rcases hy with ⟨y, rfl⟩ + rcases mul_left_surjective x y with ⟨y, rfl⟩ + conv_lhs => + rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map] + congr 2 with g + simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul] + let f' := MonoidHomClass.toMonoidHom f + show f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y + rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits] end MonoidHom From 3517336f71d10f83d643fc9838d0ade47930d32a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Mon, 10 Jun 2024 10:21:25 -0400 Subject: [PATCH 5/5] remove the old one --- Mathlib/RingTheory/IntegralDomain.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean index 9cc2e33135f161..6095f071ddd4f6 100644 --- a/Mathlib/RingTheory/IntegralDomain.lean +++ b/Mathlib/RingTheory/IntegralDomain.lean @@ -192,15 +192,6 @@ end EuclideanDivision variable [Fintype G] -theorem card_fiber_eq_of_mem_range {H : Type*} [Group H] [DecidableEq H] (f : G →* H) {x y : H} - (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) : - -- Porting note: the `filter` had an index `ₓ` that I removed. - (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by - rcases hx with ⟨x, rfl⟩ - rcases hy with ⟨y, rfl⟩ - exact card_equiv (Equiv.mulRight (x⁻¹ * y)) (by simp [mul_inv_eq_one]) -#align card_fiber_eq_of_mem_range card_fiber_eq_of_mem_range - /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero. -/ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 := by