Source: ProCGroups.GroupTheory.Conjugation
1import Mathlib.GroupTheory.QuotientGroup.Basic
3/-!
4# Conjugation on characteristic quotients
6This module constructs the automorphism induced on a characteristic quotient and uses it to
7descend conjugation by a normal subgroup to an action of the ambient quotient.
8-/
10namespace ProCGroups
12namespace Subgroup
13namespace Characteristic
15universe u
17variable {G : Type u} [Group G] {H : Subgroup G}
19/-- An automorphism descends to the quotient by a characteristic subgroup. -/
20noncomputable def quotientMulEquiv
21 (hH : H.Characteristic) (e : G ≃* G) :
22 G ⧸ H ≃* G ⧸ H := by
23 letI : H.Normal := by infer_instance
24 exact QuotientGroup.congr H H e (Subgroup.characteristic_iff_map_eq.mp hH e)
26/--
27The quotient equivalence induced by a characteristic subgroup sends representatives to
28representatives.
29-/
30@[simp] theorem quotientMulEquiv_mk
31 (hH : H.Characteristic) (e : G ≃* G) (g : G) :
32 quotientMulEquiv hH e (QuotientGroup.mk' H g) = QuotientGroup.mk' H (e g) :=
33 rfl
35end Characteristic
36end Subgroup
38end ProCGroups
40namespace ProCGroups.GroupTheory
42universe u
44/--
45If \(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.
47-/
48noncomputable def quotientConjugationOnCharacteristicQuotient
49 {G : Type u} [Group G]
50 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.Characteristic]
51 (hNactsTrivially :
52 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K) :
53 (G ⧸ N) →* MulAut (N ⧸ K) := by
54 let hKchar : K.Characteristic := inferInstance
55 letI : K.Normal := by infer_instance
56 let prequotientAction : G →* MulAut (N ⧸ K) :=
57 { toFun := fun g => ProCGroups.Subgroup.Characteristic.quotientMulEquiv hKchar
58 (MulAut.conjNormal g)
59 map_one' := by
60 ext a
61 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
62 rw [Subgroup.Characteristic.quotientMulEquiv_mk]
63 simp only [map_one, MulAut.one_apply, QuotientGroup.mk'_apply]
64 map_mul' := by
65 intro g h
66 ext a
67 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
68 change
69 QuotientGroup.mk' K ((MulAut.conjNormal (g * h)) x) =
70 ProCGroups.Subgroup.Characteristic.quotientMulEquiv hKchar (MulAut.conjNormal g)
71 (ProCGroups.Subgroup.Characteristic.quotientMulEquiv hKchar (MulAut.conjNormal h)
72 (QuotientGroup.mk' K x))
73 rw [Subgroup.Characteristic.quotientMulEquiv_mk,
74 Subgroup.Characteristic.quotientMulEquiv_mk]
75 congr 1
76 ext
77 simp only [map_mul, MulAut.mul_apply, MulAut.conjNormal_apply, mul_assoc]}
78 have hNker : N ≤ prequotientAction.ker := by
79 intro g hg
80 ext a
81 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
82 change
83 QuotientGroup.mk' K ((MulAut.conjNormal g) x) =
84 QuotientGroup.mk' K x
85 exact
86 (QuotientGroup.eq_iff_div_mem (N := K)
87 (x := (MulAut.conjNormal g) x) (y := x)).2
88 (by simpa [div_eq_mul_inv] using hNactsTrivially ⟨g, hg⟩ x)
89 exact QuotientGroup.lift N prequotientAction hNker
91/-- The algebraic conjugation action sends representatives to conjugates. -/
92@[simp] theorem quotientConjugationOnCharacteristicQuotient_mk_apply_mk
93 {G : Type u} [Group G]
94 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.Characteristic]
95 (hNactsTrivially :
96 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K)
97 (g : G) (n : N) :
98 quotientConjugationOnCharacteristicQuotient
99 (G := G) N K hNactsTrivially
100 (QuotientGroup.mk' N g) (QuotientGroup.mk' K n) =
101 QuotientGroup.mk' K ((MulAut.conjNormal g) n) := by
102 dsimp [quotientConjugationOnCharacteristicQuotient]
103 rfl
105end ProCGroups.GroupTheory