ProCGroups/Topologies/ContinuousMonoidHom.lean
1import Mathlib.Topology.Algebra.ContinuousMonoidHom
2import Mathlib.Topology.Algebra.Group.Quotient
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Topologies/ContinuousMonoidHom.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-/
18namespace MonoidHom
20universe u v
22/-- A homomorphism from a topological group to a discrete group is continuous if its kernel is
23open. -/
25 {G : Type u} {Q : Type v}
26 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27 [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
28 (f : G →* Q) (hker : IsOpen ((f.ker : Subgroup G) : Set G)) : Continuous f := by
29 classical
30 rw [continuous_discrete_rng]
31 intro y
32 by_cases hy : ∃ x : G, f x = y
33 · rcases hy with ⟨x, hx⟩
34 have hEq :
35 f ⁻¹' ({y} : Set Q) = (fun z : G => x * z) '' ((f.ker : Subgroup G) : Set G) := by
36 ext z
37 constructor
38 · intro hz
39 have hz' : f z = y := by simpa using hz
40 refine ⟨x⁻¹ * z, ?_, by simp only [mul_inv_cancel_left]⟩
41 change f (x⁻¹ * z) = 1
43 · rintro ⟨k, hk, rfl⟩
44 change f (x * k) = y
46 simpa using hk
47 rw [hEq]
48 exact isOpenMap_mul_left x _ hker
49 · have hEq : f ⁻¹' ({y} : Set Q) = ∅ := by
50 ext z
51 constructor
52 · intro hz
53 exact False.elim (hy ⟨z, hz⟩)
54 · intro hz
55 simp only [Set.mem_empty_iff_false] at hz
56 rw [hEq]
57 exact isOpen_empty
59end MonoidHom
61namespace ContinuousMonoidHom
63universe u v
65section Group
67variable {G : Type u} {H : Type v}
68variable [Group G] [TopologicalSpace G]
69variable [Group H] [TopologicalSpace H]
71/-- The inclusion of a subgroup, as a continuous monoid homomorphism for the subtype topology. -/
73 toMonoidHom := K.subtype
74 continuous_toFun := continuous_subtype_val
76/-- The continuous homomorphism associated to subgroup inclusion evaluates as the underlying element. -/
77@[simp] theorem subtype_apply (K : Subgroup G) (x : K) :
79 rfl
81/-- The quotient projection, as a continuous monoid homomorphism for the quotient topology. -/
82def quotientMk (K : Subgroup G) [K.Normal] : G →ₜ* G ⧸ K where
83 toMonoidHom := QuotientGroup.mk' K
84 continuous_toFun := continuous_quotient_mk'
86/-- The continuous quotient homomorphism evaluates to the quotient class of an element. -/
87@[simp] theorem quotientMk_apply (K : Subgroup G) [K.Normal] (x : G) :
88 quotientMk K x = QuotientGroup.mk' K x :=
89 rfl
91/-- A continuous surjective homomorphism from a compact group to a Hausdorff topological group is
92an open map. -/
94 [IsTopologicalGroup G] [IsTopologicalGroup H] [CompactSpace G] [T2Space H]
95 (f : G →ₜ* H) (hf : Function.Surjective f) :
96 IsOpenMap f := by
97 intro U hU
98 have hq : Topology.IsQuotientMap f :=
99 f.continuous_toFun.isClosedMap.isQuotientMap f.continuous_toFun hf
100 refine (hq.isOpen_preimage).1 ?_
101 have hpre :
102 f ⁻¹' (f '' U) =
103 ⋃ k : f.toMonoidHom.ker, (fun x : G => x * k.1) '' U := by
104 ext z
105 constructor
106 · intro hz
107 rcases hz with ⟨u, huU, huf⟩
108 refine Set.mem_iUnion.2
109 ⟨⟨u⁻¹ * z, ?_⟩, ⟨u, huU, by simp only [mul_inv_cancel_left]⟩⟩
110 change f.toMonoidHom (u⁻¹ * z) = 1
112 · intro hz
113 rcases Set.mem_iUnion.1 hz with ⟨k, hk⟩
114 rcases hk with ⟨u, huU, rfl⟩
115 exact ⟨u, huU, by
116 change f.toMonoidHom u = f.toMonoidHom (u * k.1)
118 rw [hpre]
119 exact isOpen_iUnion fun k => isOpenMap_mul_right k.1 U hU
121/-- Restrict a continuous homomorphism to its range, with the induced subtype topology. -/
122def rangeRestrict (f : G →ₜ* H) : G →ₜ* f.toMonoidHom.range where
123 toMonoidHom := f.toMonoidHom.rangeRestrict
124 continuous_toFun := Continuous.subtype_mk f.continuous_toFun fun x => ⟨x, rfl⟩
126/-- The range-restricted continuous homomorphism evaluates to the image element in the range. -/
127@[simp] theorem rangeRestrict_apply (f : G →ₜ* H) (x : G) :
128 f.rangeRestrict x = f.toMonoidHom.rangeRestrict x :=
129 rfl
131/-- Coercing the range-restricted homomorphism gives the original homomorphism value. -/
132@[simp] theorem coe_rangeRestrict_apply (f : G →ₜ* H) (x : G) :
133 (f.rangeRestrict x : H) = f x :=
134 rfl
136/-- The kernel of a continuous homomorphism to a `T1` group is closed. -/
137theorem isClosed_ker [T1Space H] (f : G →ₜ* H) :
138 IsClosed ((f.toMonoidHom.ker : Subgroup G) : Set G) := by
139 simpa [MonoidHom.mem_ker] using
140 (isClosed_singleton (x := (1 : H))).preimage f.continuous_toFun
142/-- The range of a continuous homomorphism from a compact space to a Hausdorff space is closed. -/
143theorem isClosed_range [CompactSpace G] [T2Space H] (f : G →ₜ* H) :
144 IsClosed ((f.toMonoidHom.range : Subgroup H) : Set H) := by
146 isCompact_univ.image f.continuous_toFun
147 have hEq : f '' (Set.univ : Set G) = ((f.toMonoidHom.range : Subgroup H) : Set H) := by
148 ext y
149 constructor
150 · rintro ⟨x, _hx, rfl⟩
151 exact ⟨x, rfl⟩
152 · rintro ⟨x, rfl⟩
153 exact ⟨x, trivial, rfl⟩
154 exact (hEq ▸ himage).isClosed
156end Group
158end ContinuousMonoidHom