Source: ProCGroups.Topologies.Conjugation
1import ProCGroups.GroupTheory.Conjugation
2import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
4/-!
5# Continuous conjugation actions
7This file bundles conjugation by a normalizing element as a continuous multiplicative
8equivalence. It also descends conjugation to quotients by topologically characteristic
9subgroups and records the formula on quotient representatives.
10-/
12open scoped Topology
14namespace ProCGroups
16namespace Subgroup
18universe u
20/-- Conjugation by an ambient element as a continuous automorphism of a normal subgroup. -/
21noncomputable def conjNormalContinuousMulEquiv
22 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
23 (N : Subgroup G) [N.Normal] (g : G) : N ≃ₜ* N :=
24 { toMulEquiv := MulAut.conjNormal g
25 continuous_toFun := by
26 apply Continuous.subtype_mk
27 change Continuous fun x : N => g * (x : G) * g⁻¹
28 exact
29 ((continuous_const : Continuous fun _ : N => g).mul continuous_subtype_val).mul
30 (continuous_const : Continuous fun _ : N => g⁻¹)
31 continuous_invFun := by
32 apply Continuous.subtype_mk
33 change Continuous fun x : N => g⁻¹ * (x : G) * (g⁻¹)⁻¹
34 exact
35 ((continuous_const : Continuous fun _ : N => g⁻¹).mul continuous_subtype_val).mul
36 (continuous_const : Continuous fun _ : N => (g⁻¹)⁻¹) }
38/-- The conjugation equivalence is evaluated by conjugating representatives. -/
39@[simp] theorem conjNormalContinuousMulEquiv_apply
40 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
41 (N : Subgroup G) [N.Normal] (g : G) (x : N) :
42 conjNormalContinuousMulEquiv N g x = MulAut.conjNormal g x :=
43 rfl
45end Subgroup
47end ProCGroups
49namespace ProCGroups.Topologies
51universe u
53/--
54Topological variant of
55\(\mathrm{ProCGroups.GroupTheory.quotientConjugationOnCharacteristicQuotient}\). It only needs
56\(K\) to be preserved by continuous automorphisms, since the conjugation maps used to define the
57action are continuous.
58-/
59noncomputable def quotientConjugationOnTopologicallyCharacteristicQuotient
60 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
61 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.TopologicallyCharacteristic]
62 (hNactsTrivially :
63 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K) :
64 (G ⧸ N) →* MulAut (N ⧸ K) := by
65 let hKchar : K.TopologicallyCharacteristic := inferInstance
66 letI : K.Normal := by infer_instance
67 let prequotientAction : G →* MulAut (N ⧸ K) :=
68 { toFun := fun g =>
69 hKchar.quotientMulEquiv (Subgroup.conjNormalContinuousMulEquiv (G := G) N g)
70 map_one' := by
71 ext a
72 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
74 simp only [Subgroup.conjNormalContinuousMulEquiv, map_one, ContinuousMulEquiv.coe_mk,
75 MulAut.one_apply,
76 QuotientGroup.mk'_apply]
77 map_mul' := by
78 intro g h
79 ext a
80 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
81 change
82 QuotientGroup.mk' K
83 ((Subgroup.conjNormalContinuousMulEquiv (G := G) N (g * h)) x) =
84 hKchar.quotientMulEquiv (Subgroup.conjNormalContinuousMulEquiv (G := G) N g)
85 (hKchar.quotientMulEquiv
86 (Subgroup.conjNormalContinuousMulEquiv (G := G) N h) (QuotientGroup.mk' K x))
89 congr 1
90 ext
91 simp only [Subgroup.conjNormalContinuousMulEquiv, map_mul, ContinuousMulEquiv.coe_mk,
92 MulAut.mul_apply,
93 MulAut.conjNormal_apply, mul_assoc]}
94 have hNker : N ≤ prequotientAction.ker := by
95 intro g hg
96 ext a
97 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
98 change
99 QuotientGroup.mk' K ((MulAut.conjNormal g) x) =
100 QuotientGroup.mk' K x
101 exact
102 (QuotientGroup.eq_iff_div_mem (N := K)
103 (x := (MulAut.conjNormal g) x) (y := x)).2
104 (by simpa [div_eq_mul_inv] using hNactsTrivially ⟨g, hg⟩ x)
105 exact QuotientGroup.lift N prequotientAction hNker
107/-- The topological conjugation action sends representatives to conjugates. -/
108@[simp] theorem quotientConjugationOnTopologicallyCharacteristicQuotient_mk_apply_mk
109 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
110 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.TopologicallyCharacteristic]
111 (hNactsTrivially :
112 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K)
113 (g : G) (n : N) :
114 quotientConjugationOnTopologicallyCharacteristicQuotient
115 (G := G) N K hNactsTrivially
116 (QuotientGroup.mk' N g) (QuotientGroup.mk' K n) =
117 QuotientGroup.mk' K ((MulAut.conjNormal g) n) := by
118 dsimp [quotientConjugationOnTopologicallyCharacteristicQuotient]
119 rfl
121end ProCGroups.Topologies