Yamaguchi Lean 4 Library
Source: ProCGroups.FreeProducts.UniversalProperty
ProCGroups/FreeProducts/UniversalProperty/Source

Source: ProCGroups.FreeProducts.UniversalProperty

1import ProCGroups.ProC.InverseLimits.Predicates
3/-!
4# Pro C Groups / Free Products / Universal Property
6This module defines the binary free pro-C universal property and its canonical
7comparison maps and equivalences.
8-/
11namespace ProCGroups.FreeProducts
12universe u
15section FreeProCProducts
18variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
19variable [Group G₁] [TopologicalSpace G₁]
20variable [Group G₂] [TopologicalSpace G₂]
21variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
23/--
24Binary free pro-\(C\) products via the strengthened universal property used elsewhere in the
25project: every pair of continuous homomorphisms into a pro-\(C\) target extends uniquely.
26-/
27structure IsFreeProCProduct
28 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
29 (ι₁ : G₁ →ₜ* F) (ι₂ : G₂ →ₜ* F) : Prop where
30 /--
31 Open normal subgroups with quotients in `C` form a neighborhood basis at one in the proposed
32 free product.
33 -/
34 hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
35 /--
36 Any pair of continuous homomorphisms from the two factors into a pro-`C` target extends to a
37 unique continuous homomorphism from `F`, with the two prescribed composites.
38 -/
39 existsUnique_lift :
40 ∀ {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
41 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K],
43 ∀ (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K),
44 ∃! φ : F →ₜ* K, φ.comp ι₁ = φ₁ ∧ φ.comp ι₂ = φ₂
47namespace IsFreeProCProduct
49variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
50variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
52/-- The universal property selects a descent morphism from a binary free product object. -/
53noncomputable def lift (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
54 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
55 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
57 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) : F →ₜ* K :=
58 Classical.choose (ExistsUnique.exists (hF.existsUnique_lift hK φ₁ φ₂))
60omit [IsTopologicalGroup F] in
61/-- The chosen free-product descent morphism has the prescribed composites. -/
62theorem lift_spec (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
63 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
64 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
66 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
67 (hF.lift hK φ₁ φ₂).comp ι₁ = φ₁ ∧ (hF.lift hK φ₁ φ₂).comp ι₂ = φ₂ :=
68 Classical.choose_spec (ExistsUnique.exists (hF.existsUnique_lift hK φ₁ φ₂))
70omit [IsTopologicalGroup F] in
71/-- The left composite of the chosen free-product descent morphism is the prescribed left leg. -/
72@[simp] theorem lift_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
73 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
74 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
76 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
77 (hF.lift hK φ₁ φ₂).comp ι₁ = φ₁ :=
78 (hF.lift_spec hK φ₁ φ₂).1
80omit [IsTopologicalGroup F] in
81/-- The right composite of the chosen free-product descent morphism is the prescribed right leg. -/
82@[simp] theorem lift_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
83 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
84 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
86 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
87 (hF.lift hK φ₁ φ₂).comp ι₂ = φ₂ :=
88 (hF.lift_spec hK φ₁ φ₂).2
90omit [IsTopologicalGroup F] in
91/-- Uniqueness of the chosen free-product descent morphism. -/
92theorem lift_unique (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
93 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
94 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
96 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K)
97 {ψ : F →ₜ* K} (hψ : ψ.comp ι₁ = φ₁ ∧ ψ.comp ι₂ = φ₂) :
98 ψ = hF.lift hK φ₁ φ₂ := by
99 exact
100 (hF.existsUnique_lift hK φ₁ φ₂).unique hψ
101 (hF.lift_spec hK φ₁ φ₂)
103/-- The distinguished descent map from a free product object to itself is the identity. -/
104@[simp] theorem lift_self (hF : IsFreeProCProduct (C := C) ι₁ ι₂) :
105 hF.lift hF.hasOpenNormalBasisInClass ι₁ ι₂ = ContinuousMonoidHom.id F := by
106 symm
107 exact hF.lift_unique hF.hasOpenNormalBasisInClass ι₁ ι₂ ⟨rfl, rfl⟩
109omit [IsTopologicalGroup F] in
110/--
111Homomorphisms out of a free-product object are equal when they agree on the canonical factors.
112-/
113theorem hom_ext (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
114 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
115 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
117 {ψ ψ' : F →ₜ* K}
118 (h₁ : ψ.comp ι₁ = ψ'.comp ι₁) (h₂ : ψ.comp ι₂ = ψ'.comp ι₂) :
119 ψ = ψ' := by
120 exact
121 (hF.existsUnique_lift hK (ψ.comp ι₁) (ψ.comp ι₂)).unique
122 ⟨rfl, rfl⟩ ⟨h₁.symm, h₂.symm⟩
124variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
125variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
126variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
128/--
129The canonical comparison morphism between two free product objects on the same pair of factors.
130-/
131noncomputable def compare (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
132 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
133 F →ₜ* F' :=
134 hF.lift hF'.hasOpenNormalBasisInClass ι₁' ι₂'
136omit [IsTopologicalGroup F] in
137/--
138The left composite of the canonical comparison map between free product objects is the
139prescribed left leg.
140-/
141@[simp 900] theorem compare_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
142 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
143 (hF.compare hF').comp ι₁ = ι₁' :=
144 hF.lift_left hF'.hasOpenNormalBasisInClass ι₁' ι₂'
146omit [IsTopologicalGroup F] in
147/--
148The right composite of the canonical comparison map between free product objects is the
149prescribed right leg.
150-/
151@[simp 900] theorem compare_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
152 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
153 (hF.compare hF').comp ι₂ = ι₂' :=
154 hF.lift_right hF'.hasOpenNormalBasisInClass ι₁' ι₂'
156/-- The canonical comparison map from a free product object to itself is the identity. -/
157@[simp 900] theorem compare_self (hF : IsFreeProCProduct (C := C) ι₁ ι₂) :
158 hF.compare hF = ContinuousMonoidHom.id F := by
159 exact hF.lift_self
161variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
162variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
163variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
165omit [IsTopologicalGroup F] in
166/-- Composition of free-product comparison maps is the expected direct comparison map. -/
167theorem compare_comp (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
168 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂')
169 (hF'' : IsFreeProCProduct (C := C) ι₁'' ι₂'') :
170 (hF'.compare hF'').comp (hF.compare hF') = hF.compare hF'' := by
171 apply hF.hom_ext hF''.hasOpenNormalBasisInClass
172 · calc
173 ((hF'.compare hF'').comp (hF.compare hF')).comp ι₁
174 = (hF'.compare hF'').comp ((hF.compare hF').comp ι₁) := by rfl
175 _ = (hF'.compare hF'').comp ι₁' := by rw [hF.compare_left hF']
176 _ = ι₁'' := hF'.compare_left hF''
177 _ = (hF.compare hF'').comp ι₁ := (hF.compare_left hF'').symm
178 · calc
179 ((hF'.compare hF'').comp (hF.compare hF')).comp ι₂
180 = (hF'.compare hF'').comp ((hF.compare hF').comp ι₂) := by rfl
181 _ = (hF'.compare hF'').comp ι₂' := by rw [hF.compare_right hF']
182 _ = ι₂'' := hF'.compare_right hF''
183 _ = (hF.compare hF'').comp ι₂ := (hF.compare_right hF'').symm
185/-- Any two binary free product objects on the same factors are canonically isomorphic. -/
186noncomputable def equiv (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
187 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
188 F ≃ₜ* F' := by
189 let φ : F →ₜ* F' := hF.compare hF'
190 let ψ : F' →ₜ* F := hF'.compare hF
191 have hleft : ψ.comp φ = ContinuousMonoidHom.id F := by
192 calc
193 ψ.comp φ = hF.compare hF := by
194 simpa [φ, ψ] using hF.compare_comp hF' hF
195 _ = ContinuousMonoidHom.id F := hF.compare_self
196 have hright : φ.comp ψ = ContinuousMonoidHom.id F' := by
197 calc
198 φ.comp ψ = hF'.compare hF' := by
199 simpa [φ, ψ] using hF'.compare_comp hF hF'
200 _ = ContinuousMonoidHom.id F' := hF'.compare_self
201 refine ContinuousMulEquiv.mk'
202 (Homeomorph.mk
203 (MonoidHom.toMulEquiv φ.toMonoidHom ψ.toMonoidHom
204 (by
205 have hleft' := congrArg ContinuousMonoidHom.toMonoidHom hleft
206 change ψ.toMonoidHom.comp φ.toMonoidHom = MonoidHom.id F at hleft'
207 exact hleft')
208 (by
209 have hright' := congrArg ContinuousMonoidHom.toMonoidHom hright
210 change φ.toMonoidHom.comp ψ.toMonoidHom = MonoidHom.id F' at hright'
211 exact hright'))
212 φ.continuous_toFun ψ.continuous_toFun)
213 ?_
214 intro x y
215 exact φ.map_mul x y
217/--
218The left composite of the canonical equivalence between free-product objects is the canonical
219left map.
220-/
221@[simp] theorem equiv_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
222 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
223 ((hF.equiv hF' : F →ₜ* F').comp ι₁) = ι₁' := by
224 exact hF.compare_left hF'
226/--
227The right composite of the canonical equivalence between free product objects is the prescribed
228right leg.
229-/
230@[simp] theorem equiv_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
231 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
232 ((hF.equiv hF' : F →ₜ* F').comp ι₂) = ι₂' := by
233 exact hF.compare_right hF'
235/-- Left-leg formula for the inverse canonical free-product equivalence. -/
236theorem equiv_symm_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
237 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
238 (((hF.equiv hF').symm : F' →ₜ* F).comp ι₁') = ι₁ := by
239 change (hF'.compare hF).comp ι₁' = ι₁
240 exact hF'.compare_left hF
242/-- Right-leg formula for the inverse canonical free-product equivalence. -/
243theorem equiv_symm_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
244 (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
245 (((hF.equiv hF').symm : F' →ₜ* F).comp ι₂') = ι₂ := by
246 change (hF'.compare hF).comp ι₂' = ι₂
247 exact hF'.compare_right hF
249end IsFreeProCProduct
252end FreeProCProducts
254end ProCGroups.FreeProducts