ProCGroups/GroupTheory/Conjugation.lean
1import Mathlib.GroupTheory.QuotientGroup.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/GroupTheory/Conjugation.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Group-theoretic support lemmas
14Basic algebraic group lemmas used by the profinite and pro-C infrastructure.
15-/
17namespace Subgroup
18namespace Characteristic
20universe u
22variable {G : Type u} [Group G] {H : Subgroup G}
24/-- An automorphism descends to the quotient by a characteristic subgroup. -/
25noncomputable def quotientMulEquiv
26 (hH : H.Characteristic) (e : G ≃* G) :
27 G ⧸ H ≃* G ⧸ H := by
28 letI : H.Normal := by infer_instance
29 exact QuotientGroup.congr H H e (Subgroup.characteristic_iff_map_eq.mp hH e)
31/-- The quotient equivalence induced by a characteristic subgroup sends representatives to
32representatives. -/
33@[simp] theorem quotientMulEquiv_mk
34 (hH : H.Characteristic) (e : G ≃* G) (g : G) :
35 hH.quotientMulEquiv e (QuotientGroup.mk' H g) = QuotientGroup.mk' H (e g) :=
36 rfl
38end Characteristic
39end Subgroup
41namespace ProCGroups.GroupTheory
43universe u
45/-- If `K` is characteristic in a normal subgroup `N` and inner conjugation by elements of `N`
46is trivial on `N/K`, then `G/N` acts on `N/K` by conjugation. -/
47noncomputable def quotientConjugationOnCharacteristicQuotient
48 {G : Type u} [Group G]
49 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.Characteristic]
50 (hNactsTrivially :
51 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K) :
52 (G ⧸ N) →* MulAut (N ⧸ K) := by
53 let hKchar : K.Characteristic := inferInstance
54 letI : K.Normal := by infer_instance
55 let prequotientAction : G →* MulAut (N ⧸ K) :=
56 { toFun := fun g => hKchar.quotientMulEquiv (MulAut.conjNormal g)
57 map_one' := by
58 ext a
59 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
62 map_mul' := by
63 intro g h
64 ext a
65 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
66 change
67 QuotientGroup.mk' K ((MulAut.conjNormal (g * h)) x) =
68 hKchar.quotientMulEquiv (MulAut.conjNormal g)
69 (hKchar.quotientMulEquiv (MulAut.conjNormal h) (QuotientGroup.mk' K x))
72 congr 1
73 ext
75 have hNker : N ≤ prequotientAction.ker := by
76 intro g hg
77 ext a
78 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
79 change
80 QuotientGroup.mk' K ((MulAut.conjNormal g) x) =
81 QuotientGroup.mk' K x
82 exact
83 (QuotientGroup.eq_iff_div_mem (N := K)
84 (x := (MulAut.conjNormal g) x) (y := x)).2
85 (by simpa [div_eq_mul_inv] using hNactsTrivially ⟨g, hg⟩ x)
86 exact QuotientGroup.lift N prequotientAction hNker
88/-- The algebraic conjugation action sends representatives to conjugates. -/
89@[simp] theorem quotientConjugationOnCharacteristicQuotient_mk_apply_mk
90 {G : Type u} [Group G]
91 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.Characteristic]
92 (hNactsTrivially :
93 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K)
94 (g : G) (n : N) :
96 (G := G) N K hNactsTrivially
97 (QuotientGroup.mk' N g) (QuotientGroup.mk' K n) =
98 QuotientGroup.mk' K ((MulAut.conjNormal g) n) := by
100 rfl
102end ProCGroups.GroupTheory