Source: ProCGroups.Topologies.ContinuousMonoidHom
1import Mathlib.Topology.Algebra.ContinuousMonoidHom
2import Mathlib.Topology.Algebra.Group.Quotient
4/-!
5# Continuous group homomorphisms
7This file provides standard continuous homomorphisms involving subgroups and quotients, proves an
8open-mapping criterion for compact-to-Hausdorff surjections, and develops range restrictions.
9Kernels and ranges are shown closed under the expected separation hypotheses.
10-/
12namespace ProCGroups
14namespace MonoidHom
16universe u v
18/--
19A homomorphism from a topological group to a discrete group is continuous if its kernel is open.
20-/
21theorem continuous_of_isOpen_ker_to_discrete
22 {G : Type u} {Q : Type v}
23 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24 [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
25 (f : G →* Q) (hker : IsOpen ((f.ker : Subgroup G) : Set G)) : Continuous f := by
26 classical
27 rw [continuous_discrete_rng]
28 intro y
29 by_cases hy : ∃ x : G, f x = y
30 · rcases hy with ⟨x, hx⟩
31 have hEq :
32 f ⁻¹' ({y} : Set Q) = (fun z : G => x * z) '' ((f.ker : Subgroup G) : Set G) := by
33 ext z
34 constructor
35 · intro hz
36 have hz' : f z = y := by simpa using hz
37 refine ⟨x⁻¹ * z, ?_, by simp only [mul_inv_cancel_left]⟩
38 change f (x⁻¹ * z) = 1
39 simp only [map_mul, map_inv, hx, hz', inv_mul_cancel]
40 · rintro ⟨k, hk, rfl⟩
41 change f (x * k) = y
42 rw [map_mul, hx]
43 simpa using hk
44 rw [hEq]
45 exact isOpenMap_mul_left x _ hker
46 · have hEq : f ⁻¹' ({y} : Set Q) = ∅ := by
47 ext z
48 constructor
49 · intro hz
50 exact False.elim (hy ⟨z, hz⟩)
51 · intro hz
52 simp only [Set.mem_empty_iff_false] at hz
53 rw [hEq]
54 exact isOpen_empty
56end MonoidHom
58namespace ContinuousMonoidHom
60universe u v
62section Group
64variable {G : Type u} {H : Type v}
65variable [Group G] [TopologicalSpace G]
66variable [Group H] [TopologicalSpace H]
68/-- The inclusion of a subgroup, as a continuous monoid homomorphism for the subtype topology. -/
69def subtype (K : Subgroup G) : K →ₜ* G where
70 toMonoidHom := K.subtype
71 continuous_toFun := continuous_subtype_val
73/--
74The continuous homomorphism induced by a subgroup inclusion evaluates to the underlying subgroup
75element.
76-/
77@[simp] theorem subtype_apply (K : Subgroup G) (x : K) :
78 subtype K x = x :=
79 rfl
81/--
82The quotient projection \(G \to G/K\), bundled as a continuous monoid homomorphism for the
83quotient topology.
84-/
85def quotientMk (K : Subgroup G) [K.Normal] : G →ₜ* G ⧸ K where
86 toMonoidHom := QuotientGroup.mk' K
87 continuous_toFun := continuous_quotient_mk'
89/--
90The continuous quotient homomorphism evaluates by taking the quotient class of the input
91element.
92-/
93@[simp] theorem quotientMk_apply (K : Subgroup G) [K.Normal] (x : G) :
94 quotientMk K x = QuotientGroup.mk' K x :=
95 rfl
97/--
98A continuous surjective homomorphism from a compact group to a Hausdorff topological group is an
99open map.
100-/
101theorem isOpenMap_of_surjective_compact_t2
102 [IsTopologicalGroup G] [CompactSpace G] [T2Space H]
103 (f : G →ₜ* H) (hf : Function.Surjective f) :
104 IsOpenMap f := by
105 intro U hU
106 have hq : Topology.IsQuotientMap f :=
107 f.continuous_toFun.isClosedMap.isQuotientMap f.continuous_toFun hf
108 refine (hq.isOpen_preimage).1 ?_
109 have hpre :
110 f ⁻¹' (f '' U) =
111 ⋃ k : f.toMonoidHom.ker, (fun x : G => x * k.1) '' U := by
112 ext z
113 constructor
114 · intro hz
115 rcases hz with ⟨u, huU, huf⟩
116 refine Set.mem_iUnion.2
117 ⟨⟨u⁻¹ * z, ?_⟩, ⟨u, huU, by simp only [mul_inv_cancel_left]⟩⟩
118 change f.toMonoidHom (u⁻¹ * z) = 1
119 simp only [_root_.ContinuousMonoidHom.coe_toMonoidHom, map_mul, map_inv,
120 MonoidHom.coe_coe, huf, inv_mul_cancel]
121 · intro hz
122 rcases Set.mem_iUnion.1 hz with ⟨k, hk⟩
123 rcases hk with ⟨u, huU, rfl⟩
124 exact ⟨u, huU, by
125 change f.toMonoidHom u = f.toMonoidHom (u * k.1)
126 rw [map_mul, show f.toMonoidHom k.1 = 1 from k.2, mul_one]⟩
127 rw [hpre]
128 exact isOpen_iUnion fun k => isOpenMap_mul_right k.1 U hU
130/-- A continuous homomorphism restricts to its range with the induced subtype topology. -/
131def rangeRestrict (f : G →ₜ* H) : G →ₜ* f.toMonoidHom.range where
132 toMonoidHom := f.toMonoidHom.rangeRestrict
133 continuous_toFun := Continuous.subtype_mk f.continuous_toFun fun x => ⟨x, rfl⟩
135/--
136The range-restricted continuous homomorphism evaluates to the image element together with its
137range-membership certificate.
138-/
139@[simp] theorem rangeRestrict_apply (f : G →ₜ* H) (x : G) :
140 f.rangeRestrict x = f.toMonoidHom.rangeRestrict x :=
141 rfl
143/--
144Coercing the range-restricted homomorphism back to the codomain recovers the original
145homomorphism value.
146-/
147@[simp] theorem coe_rangeRestrict_apply (f : G →ₜ* H) (x : G) :
148 (f.rangeRestrict x : H) = f x :=
149 rfl
151/-- The kernel of a continuous homomorphism to a \(T_1\) group is closed. -/
152theorem isClosed_ker [T1Space H] (f : G →ₜ* H) :
153 IsClosed ((f.toMonoidHom.ker : Subgroup G) : Set G) := by
154 have hker :
155 ((f.toMonoidHom.ker : Subgroup G) : Set G) =
156 f ⁻¹' ({1} : Set H) := by
157 ext x
158 change (f x = 1) ↔ f x ∈ ({1} : Set H)
159 simp only [Set.mem_singleton_iff]
160 rw [hker]
161 exact (isClosed_singleton (x := (1 : H))).preimage f.continuous_toFun
163/-- The range of a continuous homomorphism from a compact space to a Hausdorff space is closed. -/
164theorem isClosed_range [CompactSpace G] [T2Space H] (f : G →ₜ* H) :
165 IsClosed ((f.toMonoidHom.range : Subgroup H) : Set H) := by
166 have himage : IsCompact (f '' (Set.univ : Set G)) :=
167 isCompact_univ.image f.continuous_toFun
168 have hEq : f '' (Set.univ : Set G) = ((f.toMonoidHom.range : Subgroup H) : Set H) := by
169 ext y
170 constructor
171 · rintro ⟨x, _hx, rfl⟩
172 exact ⟨x, rfl⟩
173 · rintro ⟨x, rfl⟩
174 exact ⟨x, trivial, rfl⟩
175 exact (hEq ▸ himage).isClosed
177end Group
179end ContinuousMonoidHom
181end ProCGroups