ProCGroups/Topologies/Conjugation.lean
1import ProCGroups.GroupTheory.Conjugation
2import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Topologies/Conjugation.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Topological group constructions
15Topological subgroup, quotient, continuous homomorphism, continuous equivalence, conjugation, and full-subgroup-topology lemmas.
16-/
18open scoped Topology
20namespace Subgroup
22universe u
24/-- Conjugation by an ambient element as a continuous automorphism of a normal subgroup. -/
25noncomputable def conjNormalContinuousMulEquiv
26 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
27 (N : Subgroup G) [N.Normal] (g : G) : N ≃ₜ* N :=
28 { toMulEquiv := MulAut.conjNormal g
29 continuous_toFun := by
30 apply Continuous.subtype_mk
31 change Continuous fun x : N => g * (x : G) * g⁻¹
32 simpa [mul_assoc] using
33 ((continuous_const : Continuous fun _ : N => g).mul continuous_subtype_val).mul
34 (continuous_const : Continuous fun _ : N => g⁻¹)
35 continuous_invFun := by
36 apply Continuous.subtype_mk
37 change Continuous fun x : N => g⁻¹ * (x : G) * (g⁻¹)⁻¹
38 simpa [mul_assoc] using
39 ((continuous_const : Continuous fun _ : N => g⁻¹).mul continuous_subtype_val).mul
40 (continuous_const : Continuous fun _ : N => (g⁻¹)⁻¹) }
42@[simp] theorem conjNormalContinuousMulEquiv_apply
43 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
44 (N : Subgroup G) [N.Normal] (g : G) (x : N) :
45 N.conjNormalContinuousMulEquiv g x = MulAut.conjNormal g x :=
46 rfl
48end Subgroup
50namespace ProCGroups.Topologies
52universe u
54/-- Topological variant of `ProCGroups.GroupTheory.quotientConjugationOnCharacteristicQuotient`.
55It only needs `K` to be preserved by continuous automorphisms, since the conjugation maps used
56to define the action are continuous. -/
57noncomputable def quotientConjugationOnTopologicallyCharacteristicQuotient
58 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
59 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.TopologicallyCharacteristic]
60 (hNactsTrivially :
61 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K) :
62 (G ⧸ N) →* MulAut (N ⧸ K) := by
63 let hKchar : K.TopologicallyCharacteristic := inferInstance
64 letI : K.Normal := by infer_instance
65 let prequotientAction : G →* MulAut (N ⧸ K) :=
66 { toFun := fun g =>
67 hKchar.quotientMulEquiv (Subgroup.conjNormalContinuousMulEquiv (G := G) N g)
68 map_one' := by
69 ext a
70 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
72 simp only [Subgroup.conjNormalContinuousMulEquiv, map_one, ContinuousMulEquiv.coe_mk, MulAut.one_apply,
73 QuotientGroup.mk'_apply]
74 map_mul' := by
75 intro g h
76 ext a
77 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
78 change
79 QuotientGroup.mk' K
80 ((Subgroup.conjNormalContinuousMulEquiv (G := G) N (g * h)) x) =
81 hKchar.quotientMulEquiv (Subgroup.conjNormalContinuousMulEquiv (G := G) N g)
82 (hKchar.quotientMulEquiv
83 (Subgroup.conjNormalContinuousMulEquiv (G := G) N h) (QuotientGroup.mk' K x))
86 congr 1
87 ext
88 simp only [Subgroup.conjNormalContinuousMulEquiv, map_mul, ContinuousMulEquiv.coe_mk, MulAut.mul_apply,
89 MulAut.conjNormal_apply, mul_assoc]}
90 have hNker : N ≤ prequotientAction.ker := by
91 intro g hg
92 ext a
93 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective K a
94 change
95 QuotientGroup.mk' K ((MulAut.conjNormal g) x) =
96 QuotientGroup.mk' K x
97 exact
98 (QuotientGroup.eq_iff_div_mem (N := K)
99 (x := (MulAut.conjNormal g) x) (y := x)).2
100 (by simpa [div_eq_mul_inv] using hNactsTrivially ⟨g, hg⟩ x)
101 exact QuotientGroup.lift N prequotientAction hNker
103/-- The topological conjugation action sends representatives to conjugates. -/
105 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
106 (N : Subgroup G) [N.Normal] (K : Subgroup N) [K.TopologicallyCharacteristic]
107 (hNactsTrivially :
108 ∀ n x : N, (((MulAut.conjNormal (n : G)) x) * x⁻¹ : N) ∈ K)
109 (g : G) (n : N) :
111 (G := G) N K hNactsTrivially
112 (QuotientGroup.mk' N g) (QuotientGroup.mk' K n) =
113 QuotientGroup.mk' K ((MulAut.conjNormal g) n) := by
115 rfl
117end ProCGroups.Topologies