feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522)

This is the core of the work on the centralizer of a permutation.
It is the sequel of several PR which lay out basic useful results.

Let `α : Type` with `Fintype α` (and `DecidableEq α`).
The main goal of this file is to compute the cardinality of
conjugacy classes in `Equiv.Perm α`.
Every `g : Equiv.Perm α` has a `cycleType α : Multiset ℕ`.
By `Equiv.Perm.isConj_iff_cycleType_eq`,
two permutations are conjugate in `Equiv.Perm α` iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

A subsequent PR #17047 treats the case of the alternating group.



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Author: 3 people

Mathlib.lean

@@ -3362,6 +3362,7 @@ import Mathlib.GroupTheory.OreLocalization.Cardinality
 import Mathlib.GroupTheory.OreLocalization.OreSet
 import Mathlib.GroupTheory.PGroup
 import Mathlib.GroupTheory.Perm.Basic
+import Mathlib.GroupTheory.Perm.Centralizer
 import Mathlib.GroupTheory.Perm.Closure
 import Mathlib.GroupTheory.Perm.ClosureSwap
 import Mathlib.GroupTheory.Perm.ConjAct

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -151,6 +151,18 @@ theorem card_le_card_group [Finite G] : Nat.card H ≤ Nat.card G :=
 theorem card_le_of_le {H K : Subgroup G} [Finite K] (h : H ≤ K) : Nat.card H ≤ Nat.card K :=
   Nat.card_le_card_of_injective _ (Subgroup.inclusion_injective h)
 
+@[to_additive]
+theorem card_map_of_injective {H : Type*} [Group H] {K : Subgroup G} {f : G →* H}
+    (hf : Function.Injective f) :
+    Nat.card (map f K) = Nat.card K := by
+  -- simp only [← SetLike.coe_sort_coe]
+  apply Nat.card_image_of_injective hf
+
+@[to_additive]
+theorem card_subtype (K : Subgroup G) (L : Subgroup K) :
+    Nat.card (map K.subtype L) = Nat.card L :=
+  card_map_of_injective K.subtype_injective
+
 end Subgroup
 
 namespace Subgroup
@@ -275,4 +287,14 @@ Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.finty
 instance fintypeRange [Fintype G] [DecidableEq N] (f : G →* N) : Fintype (range f) :=
   Set.fintypeRange f
 
+lemma _root_.Fintype.card_coeSort_mrange {M N : Type*} [Monoid M] [Monoid N] [Fintype M]
+    [DecidableEq N] {f : M →* N} (hf : Function.Injective f) :
+    Fintype.card (mrange f) = Fintype.card M :=
+  Set.card_range_of_injective hf
+
+lemma _root_.Fintype.card_coeSort_range [Fintype G] [DecidableEq N] {f : G →* N}
+    (hf : Function.Injective f) :
+    Fintype.card (range f) = Fintype.card G :=
+  Set.card_range_of_injective hf
+
 end MonoidHom

Mathlib/GroupTheory/NoncommCoprod.lean

@@ -5,6 +5,9 @@ Authors: Antoine Chambert-Loir
 -/
 import Mathlib.Algebra.Group.Commute.Hom
 import Mathlib.Algebra.Group.Prod
+import Mathlib.Algebra.Group.Subgroup.Ker
+import Mathlib.Algebra.Group.Subgroup.Lattice
+import Mathlib.Order.Disjoint
 
 /-!
 # Canonical homomorphism from a pair of monoids
@@ -53,7 +56,6 @@ theorem noncommCoprod_apply' (comm) (mn : M × N) :
     (f.noncommCoprod g comm) mn = g mn.2 * f mn.1 := by
   rw [← comm, noncommCoprod_apply]
 
-
 @[to_additive]
 theorem comp_noncommCoprod {Q : Type*} [Semigroup Q] (h : P →ₙ* Q)
     (comm : ∀ m n, Commute (f m) (g n)) :
@@ -114,4 +116,38 @@ theorem comp_noncommCoprod {Q : Type*} [Monoid Q] (h : P →* Q) :
       (h.comp f).noncommCoprod (h.comp g) (fun m n ↦ (comm m n).map h) :=
   ext fun x => by simp
 
+section group
+
+open Subgroup
+
+lemma noncommCoprod_injective {M N P : Type*} [Group M] [Group N] [Group P]
+    (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) :
+    Function.Injective (noncommCoprod f g comm) ↔
+      (Function.Injective f ∧ Function.Injective g ∧ _root_.Disjoint f.range g.range) := by
+  simp only [injective_iff_map_eq_one, disjoint_iff_inf_le,
+    noncommCoprod_apply, Prod.forall, Prod.mk_eq_one]
+  refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
+  · simpa using h x 1
+  · simpa using h 1 x
+  · intro x ⟨⟨y, hy⟩, z, hz⟩
+    rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy
+  · intro ⟨hf, hg, hp⟩ a b h
+    have key := hp ⟨⟨a⁻¹, by rwa [map_inv, inv_eq_iff_mul_eq_one]⟩, b, rfl⟩
+    exact ⟨hf a (by rwa [key, mul_one] at h), hg b key⟩
+
+lemma noncommCoprod_range {M N P : Type*} [Group M] [Group N] [Group P]
+    (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) :
+    (noncommCoprod f g comm).range = f.range ⊔ g.range := by
+  apply le_antisymm
+  · rintro - ⟨a, rfl⟩
+    exact mul_mem (mem_sup_left ⟨a.1, rfl⟩) (mem_sup_right ⟨a.2, rfl⟩)
+  · rw [sup_le_iff]
+    constructor
+    · rintro - ⟨a, rfl⟩
+      exact ⟨(a, 1), by rw [noncommCoprod_apply, map_one, mul_one]⟩
+    · rintro - ⟨a, rfl⟩
+      exact ⟨(1, a), by rw [noncommCoprod_apply, map_one, one_mul]⟩
+
+end group
+
 end MonoidHom

Mathlib/GroupTheory/Perm/Basic.lean

@@ -399,6 +399,13 @@ theorem mem_iff_ofSubtype_apply_mem (f : Perm (Subtype p)) (x : α) :
     simpa only [h, true_iff, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2
   else by simp [h, ofSubtype_apply_of_not_mem f h]
 
+theorem ofSubtype_injective : Function.Injective (ofSubtype : Perm (Subtype p) → Perm α) := by
+  intro x y h
+  rw [Perm.ext_iff] at h ⊢
+  intro a
+  specialize h a
+  rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h
+
 @[simp]
 theorem subtypePerm_ofSubtype (f : Perm (Subtype p)) :
     subtypePerm (ofSubtype f) (mem_iff_ofSubtype_apply_mem f) = f :=