Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Morphism
ProCGroups/FoxDifferential/Completed/FreeProC/Uniqueness/Morphism/Source

Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Morphism

1import ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift
3/-!
4# Fox differential: completed — free pro-\(C\) — uniqueness — morphism
6The principal declarations in this module are:
8- `freeProCZCCompletedFoxSemidirectLiftMorphism_unique`
9 Categorical completed Fox semidirect morphisms from a free pro-\(C\) source are unique once their
10 generator values are prescribed.
11- `freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components`
12 Componentwise uniqueness for categorical completed Fox semidirect morphisms from a free pro-\(C\)
13 source.
14- `existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism`
15 Existence and uniqueness of the categorical completed Fox semidirect morphism from a free
16 pro-\(C\) source.
17- `existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components`
18 Componentwise existence and uniqueness of the categorical completed Fox semidirect morphism from a
19 free pro-\(C\) source.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups.FreeProC
28universe u
30variable {C : ProCGroups.FiniteGroupClass.{u}}
31variable {X F H : Type u}
32variable [TopologicalSpace X]
33variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
34variable [DecidableEq X]
35variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
37variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
38variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
39variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
40variable [T2Space (ZCCompletedFoxSemidirect C X H)]
41variable [TotallyDisconnectedSpace
42 (ZCCompletedFoxSemidirect C X H)]
44/--
45Categorical completed Fox semidirect morphisms from a free pro-\(C\) source are unique once
46their generator values are prescribed.
47-/
48theorem freeProCZCCompletedFoxSemidirectLiftMorphism_unique
51 (ZCCompletedFoxSemidirect C X H))
52 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
53 (φ : X → H)
54 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
55 (f :
56 ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
58 (ProfiniteGrp.of
59 (ZCCompletedFoxSemidirect C X H))
60 hTargetC)
61 (hgenerator :
62 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x) :
63 f = freeProCZCCompletedFoxSemidirectLiftMorphism
64 (C := C) hFC hTargetC hι φ hφ := by
66 apply ContinuousMonoidHom.toMonoidHom_injective
67 exact congrArg
68 (fun h : F →ₜ* ZCCompletedFoxSemidirect C X H => h.toMonoidHom)
69 (hι.liftHom_unique
70 hTargetC
71 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ
72 (f := ProCGrp.continuousHom f) hgenerator)
74/--
75Componentwise uniqueness for categorical completed Fox semidirect morphisms from a free
76pro-\(C\) source.
77-/
78theorem freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components
81 (ZCCompletedFoxSemidirect C X H))
82 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
83 (φ : X → H)
84 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
85 (f :
86 ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
88 (ProfiniteGrp.of
89 (ZCCompletedFoxSemidirect C X H))
90 hTargetC)
91 (hleft :
92 ∀ x : X, (f (ι x)).left =
93 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
94 (hright : ∀ x : X, (f (ι x)).right = φ x) :
95 f = freeProCZCCompletedFoxSemidirectLiftMorphism
96 (C := C) hFC hTargetC hι φ hφ := by
97 apply freeProCZCCompletedFoxSemidirectLiftMorphism_unique
98 (C := C) hFC hTargetC hι φ hφ f
99 intro x
100 apply ZCCompletedFoxSemidirect.ext
101 · exact hleft x
102 · exact hright x
104/--
105Existence and uniqueness of the categorical completed Fox semidirect morphism from a free
106pro-\(C\) source.
107-/
108theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism
111 (ZCCompletedFoxSemidirect C X H))
112 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
113 (φ : X → H)
114 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
115 ∃! f :
116 ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
118 (ProfiniteGrp.of
119 (ZCCompletedFoxSemidirect C X H))
120 hTargetC,
121 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x := by
122 refine ⟨freeProCZCCompletedFoxSemidirectLiftMorphism
123 (C := C) hFC hTargetC hι φ hφ, ?_, ?_⟩
124 · exact freeProCZCCompletedFoxSemidirectLiftMorphism_generator
125 (C := C) hFC hTargetC hι φ hφ
126 · intro f hf
127 exact freeProCZCCompletedFoxSemidirectLiftMorphism_unique
128 (C := C) hFC hTargetC hι φ hφ f hf
130/--
131Componentwise existence and uniqueness of the categorical completed Fox semidirect morphism from
132a free pro-\(C\) source.
133-/
134theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components
137 (ZCCompletedFoxSemidirect C X H))
138 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
139 (φ : X → H)
140 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
141 ∃! f :
142 ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
144 (ProfiniteGrp.of
145 (ZCCompletedFoxSemidirect C X H))
146 hTargetC,
147 (∀ x : X, (f (ι x)).left =
148 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
149 ∀ x : X, (f (ι x)).right = φ x := by
150 refine ⟨freeProCZCCompletedFoxSemidirectLiftMorphism
151 (C := C) hFC hTargetC hι φ hφ, ?_, ?_⟩
152 · exact
153 ⟨freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator
154 (C := C) hFC hTargetC hι φ hφ,
155 freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator
156 (C := C) hFC hTargetC hι φ hφ⟩
157 · intro f hf
158 exact freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components
159 (C := C) hFC hTargetC hι φ hφ f hf.1 hf.2
161end
163end FoxDifferential