Yamaguchi Lean 4 Library
ProCGroups/Completion/UniversalProperty.lean
ProCGroups/Completion/UniversalProperty/Source

ProCGroups/Completion/UniversalProperty.lean

1import ProCGroups.ProC.GroupPredicate
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Completion/UniversalProperty.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C completion and finite quotient systems
14Organizes finite quotient systems, completion maps, finite-target factorization, and the universal property of pro-C completion.
15-/
17open scoped Topology
19namespace ProCGroups.Completion
21universe u v
25/-- An abstract pro-`C` completion of a topological group. -/
28 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29 (Ghat : Type u) [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
30 (ι : G →ₜ* Ghat) : Prop where
31 isProC : ProC (G := Ghat)
32 denseRange : DenseRange ι
34 ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H],
35 ProC (G := H) →
36 ∀ (φ : G →ₜ* H), ∃! φbar : Ghat →ₜ* H, φbar.comp ι = φ
40variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
41variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
42variable {ι : G →ₜ* Ghat}
44/-- The continuous lift supplied by the pro-`C` completion universal property. -/
45noncomputable def lift
46 (hι : IsProCCompletion ProC G Ghat ι)
47 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
48 (hH : ProC (G := H)) (φ : G →ₜ* H) :
49 Ghat →ₜ* H :=
50 Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hH φ))
52/-- The universal-property lift is continuous and extends the given homomorphism along the completion map. -/
53theorem lift_spec
54 (hι : IsProCCompletion ProC G Ghat ι)
55 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
56 (hH : ProC (G := H)) (φ : G →ₜ* H) :
57 (hι.lift hH φ).comp ι = φ :=
58 Classical.choose_spec (ExistsUnique.exists (hι.existsUnique_lift hH φ))
60/-- The universal-property lift is the unique continuous map extending the given homomorphism. -/
61theorem lift_unique
62 (hι : IsProCCompletion ProC G Ghat ι)
63 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
64 (hH : ProC (G := H)) (φ : G →ₜ* H)
65 {f : Ghat →ₜ* H} (hfac : f.comp ι = φ) :
66 f = hι.lift hH φ := by
67 rcases hι.existsUnique_lift hH φ with ⟨g, hg, huniq⟩
68 have hchosen : hι.lift hH φ = g := huniq _ (hι.lift_spec hH φ)
69 exact (huniq _ hfac).trans hchosen.symm
71/-- Continuous homomorphisms out of a pro-`C` completion are determined by the dense source. -/
72theorem hom_ext
73 (hι : IsProCCompletion ProC G Ghat ι)
74 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
75 (hH : ProC (G := H))
76 {f g : Ghat →ₜ* H}
77 (hfg : f.comp ι = g.comp ι) :
78 f = g := by
79 have hf_lift : f = hι.lift hH (f.comp ι) :=
80 hι.lift_unique hH (f.comp ι) rfl
81 have hg_lift : g = hι.lift hH (f.comp ι) :=
82 hι.lift_unique hH (f.comp ι) hfg.symm
83 exact hf_lift.trans hg_lift.symm
85/-- The lift of the completion map to the completion itself is the identity. -/
86@[simp] theorem lift_self_eq_id
87 (hι : IsProCCompletion ProC G Ghat ι) :
88 hι.lift hι.isProC ι = ContinuousMonoidHom.id Ghat := by
89 symm
90 exact hι.lift_unique hι.isProC ι rfl
92variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
93variable {ι₂ : G →ₜ* Ghat₂}
95/-- The canonical comparison map between two pro-`C` completions of the same group. -/
96noncomputable def comparison
97 (h₁ : IsProCCompletion ProC G Ghat ι)
98 (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) : Ghat →ₜ* Ghat₂ :=
99 h₁.lift h₂.isProC ι₂
101/-- The comparison map between two pro-`C` completions agrees with the second completion map on the source. -/
103 (h₁ : IsProCCompletion ProC G Ghat ι)
104 (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) :
105 (h₁.comparison h₂).comp ι = ι₂ :=
106 h₁.lift_spec h₂.isProC ι₂
108/-- The two comparison maps between pro-`C` completions compose to the identity. -/
109@[simp 900] theorem comparison_comp_eq_id
110 (h₁ : IsProCCompletion ProC G Ghat ι)
111 (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) :
112 (h₂.comparison h₁).comp (h₁.comparison h₂) = ContinuousMonoidHom.id Ghat := by
113 let e12 : Ghat →ₜ* Ghat₂ := h₁.comparison h₂
114 let e21 : Ghat₂ →ₜ* Ghat := h₂.comparison h₁
115 have he12 : e12.comp ι = ι₂ := h₁.comparison_spec h₂
116 have he21 : e21.comp ι₂ = ι := h₂.comparison_spec h₁
117 have hfac : (e21.comp e12).comp ι = ι := by
118 ext x
119 have h12 : e12 (ι x) = ι₂ x := congrArg (fun f : G →ₜ* Ghat₂ => f x) he12
120 have h21 : e21 (ι₂ x) = ι x := congrArg (fun f : G →ₜ* Ghat => f x) he21
121 simpa [MonoidHom.comp_apply, h12] using h21
122 calc
123 e21.comp e12 = h₁.lift h₁.isProC ι :=
124 h₁.lift_unique h₁.isProC ι hfac
125 _ = ContinuousMonoidHom.id Ghat := h₁.lift_self_eq_id
127/-- The canonical multiplicative homeomorphism between two pro-`C` completions of the same
128topological group. -/
129noncomputable def continuousMulEquiv
130 (h₁ : IsProCCompletion ProC G Ghat ι)
131 (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) : Ghat ≃ₜ* Ghat₂ :=
132 let f : Ghat →ₜ* Ghat₂ := h₁.comparison h₂
133 let g : Ghat₂ →ₜ* Ghat := h₂.comparison h₁
134 { toMulEquiv :=
135 { toFun := f
136 invFun := g
137 left_inv := by
138 intro x
139 have hgf : g.comp f = ContinuousMonoidHom.id Ghat := h₁.comparison_comp_eq_id h₂
140 exact congrArg (fun h : Ghat →ₜ* Ghat => h x) hgf
141 right_inv := by
142 intro x
143 have hfg : f.comp g = ContinuousMonoidHom.id Ghat₂ := h₂.comparison_comp_eq_id h₁
144 exact congrArg (fun h : Ghat₂ →ₜ* Ghat₂ => h x) hfg
145 map_mul' := f.map_mul }
146 continuous_toFun := f.continuous_toFun
147 continuous_invFun := g.continuous_toFun }
149/-- The canonical equivalence between pro-`C` completions sends one completion map to the other. -/
151 (h₁ : IsProCCompletion ProC G Ghat ι)
152 (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) (x : G) :
153 h₁.continuousMulEquiv h₂ (ι x) = ι₂ x := by
155 congrArg (fun f : G →ₜ* Ghat₂ => f x) (h₁.comparison_spec h₂)
157/-- The inverse canonical equivalence between pro-`C` completions sends the second completion map back to the first. -/
159 (h₁ : IsProCCompletion ProC G Ghat ι)
160 (h₂ : IsProCCompletion ProC G Ghat₂ ι₂) (x : G) :
161 (h₁.continuousMulEquiv h₂).symm (ι₂ x) = ι x := by
163 congrArg (fun f : G →ₜ* Ghat => f x) (h₂.comparison_spec h₁)
167end ProCGroups.Completion