Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Lift
1import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom
3/-!
4# Fox differential: completed — free pro-\(C\) — uniqueness — lift
6The principal declarations in this module are:
8- `freeProCZCCompletedFoxSemidirectLift_unique`
9 Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique once their
10 generator values are prescribed.
11- `freeProCZCCompletedFoxSemidirectLift_unique_of_components`
12 Componentwise uniqueness for continuous completed Fox semidirect lifts from a free pro-\(C\)
13 source.
14- `freeProCZCCompletedFoxSemidirectLiftHom_unique`
15 Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique once
16 their generator values are prescribed.
17- `freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components`
18 Componentwise uniqueness for continuous completed Fox semidirect homomorphisms from a free
19 pro-\(C\) source.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups.FreeProC
28universe u
31variable {C : ProCGroups.FiniteGroupClass.{u}}
32variable {X F H : Type u}
33variable [TopologicalSpace X]
34variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
35variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
36variable [DecidableEq X]
37variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
38variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
39variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
41section ProfiniteTarget
43variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
44variable [T2Space (ZCCompletedFoxSemidirect C X H)]
45variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
47/--
48Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique once their
49generator values are prescribed.
50-/
51theorem freeProCZCCompletedFoxSemidirectLift_unique
52 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
53 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
54 (φ : X → H)
55 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
56 (f : F →* ZCCompletedFoxSemidirect C X H)
57 (hf : Continuous f)
58 (hgenerator :
59 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x) :
60 f = freeProCZCCompletedFoxSemidirectLift
61 (C := C) hι htarget φ hφ :=
62 hι.lift_unique htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
63 hφ hf hgenerator
65/--
66Componentwise uniqueness for continuous completed Fox semidirect lifts from a free pro-\(C\)
67source.
68-/
69theorem freeProCZCCompletedFoxSemidirectLift_unique_of_components
70 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
71 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
72 (φ : X → H)
73 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
74 (f : F →* ZCCompletedFoxSemidirect C X H)
75 (hf : Continuous f)
76 (hleft :
77 ∀ x : X, (f (ι x)).left =
78 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
79 (hright : ∀ x : X, (f (ι x)).right = φ x) :
80 f = freeProCZCCompletedFoxSemidirectLift
81 (C := C) hι htarget φ hφ := by
82 apply freeProCZCCompletedFoxSemidirectLift_unique
83 (C := C) hι htarget φ hφ f hf
84 intro x
85 apply ZCCompletedFoxSemidirect.ext
86 · exact hleft x
87 · exact hright x
89/--
90Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique once
91their generator values are prescribed.
92-/
93theorem freeProCZCCompletedFoxSemidirectLiftHom_unique
94 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
95 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
96 (φ : X → H)
97 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
98 (f : F →ₜ* ZCCompletedFoxSemidirect C X H)
99 (hgenerator :
100 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x) :
101 f = freeProCZCCompletedFoxSemidirectLiftHom
102 (C := C) hι htarget φ hφ :=
103 hι.liftHom_unique htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
104 hφ hgenerator
106/--
107Componentwise uniqueness for continuous completed Fox semidirect homomorphisms from a free
108pro-\(C\) source.
109-/
110theorem freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components
111 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
112 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
113 (φ : X → H)
114 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
115 (f : F →ₜ* ZCCompletedFoxSemidirect C X H)
116 (hleft :
117 ∀ x : X, (f (ι x)).left =
118 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
119 (hright : ∀ x : X, (f (ι x)).right = φ x) :
120 f = freeProCZCCompletedFoxSemidirectLiftHom
121 (C := C) hι htarget φ hφ := by
122 apply freeProCZCCompletedFoxSemidirectLiftHom_unique
123 (C := C) hι htarget φ hφ f
124 intro x
125 apply ZCCompletedFoxSemidirect.ext
126 · exact hleft x
127 · exact hright x
129/--
130Existence and uniqueness of the continuous completed Fox semidirect homomorphism from a free
131pro-\(C\) source.
132-/
133theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftHom
134 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
135 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
136 (φ : X → H)
137 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
138 ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
139 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x := by
140 refine ⟨freeProCZCCompletedFoxSemidirectLiftHom
141 (C := C) hι htarget φ hφ, ?_, ?_⟩
142 · exact freeProCZCCompletedFoxSemidirectLiftHom_generator
143 (C := C) hι htarget φ hφ
144 · intro f hf
145 exact freeProCZCCompletedFoxSemidirectLiftHom_unique
146 (C := C) hι htarget φ hφ f hf
148/--
149Componentwise existence and uniqueness of the continuous completed Fox semidirect homomorphism
150from a free pro-\(C\) source.
151-/
152theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_components
153 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
154 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
155 (φ : X → H)
156 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
157 ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
158 (∀ x : X, (f (ι x)).left =
159 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
160 ∀ x : X, (f (ι x)).right = φ x := by
161 refine ⟨freeProCZCCompletedFoxSemidirectLiftHom
162 (C := C) hι htarget φ hφ, ?_, ?_⟩
163 · exact ⟨
164 freeProCZCCompletedFoxSemidirectLiftHom_left_generator
165 (C := C) hι htarget φ hφ,
166 freeProCZCCompletedFoxSemidirectLiftHom_right_generator
167 (C := C) hι htarget φ hφ⟩
168 · intro f hf
169 exact freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components
170 (C := C) hι htarget φ hφ f hf.1 hf.2
172end ProfiniteTarget
174end
176end FoxDifferential