FoxDifferential/Completed/FreeProC/Uniqueness/Derivative.lean
1import FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FreeProC/Uniqueness/Derivative.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free pro-C completed Fox calculus
14Free pro-C sources are treated through completed Fox derivatives, stage projections, density arguments, and semidirect lift formulas.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.FreeProC
22universe u
25variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
26variable {X F H : Type u}
27variable [TopologicalSpace X]
28variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
29variable [DecidableEq X]
30variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
31variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
32variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
34/-- Any continuous semidirect lift with the prescribed generator components has the canonical
35free pro-`C` completed Fox derivative vector as its left component. -/
37 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
38 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
39 (φ : X → H)
40 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
41 (f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
42 (hf : Continuous f)
43 (hleft :
44 ∀ x : X, (f (ι x)).left =
45 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
46 (hright : ∀ x : X, (f (ι x)).right = φ x) :
47 (fun g : F => (f g).left) =
49 (ProC := ProC) hι htarget φ hφ := by
50 have hgenerator :
51 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
52 intro x
53 apply ZCCompletedFoxSemidirect.ext
54 · exact hleft x
55 · exact hright x
56 have hf_eq := hι.lift_unique htarget
57 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ hf hgenerator
58 funext g
59 rw [hf_eq]
60 rfl
62/-- Continuous completed crossed differentials on a free pro-`C` source are uniquely determined
65 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
66 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
67 (ψ : F →* H) (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
68 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
69 (hcontinuous :
71 (X := X) ψ delta hdelta))
72 (hbasis :
73 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
74 delta =
76 (ProC := ProC) hι htarget (fun x : X => ψ (ι x))
78 (ProC := ProC) hι ψ delta hdelta hcontinuous hbasis) := by
79 have hleft :
80 ∀ x : X,
82 (X := X) ψ delta hdelta (ι x)).left =
83 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
84 intro x
85 exact hbasis x
86 have hright :
87 ∀ x : X,
89 (X := X) ψ delta hdelta (ι x)).right = ψ (ι x) := by
90 intro x
91 rfl
92 have hunique := freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect
93 (ProC := ProC) hι htarget (fun x : X => ψ (ι x))
95 (ProC := ProC) hι ψ delta hdelta hcontinuous hbasis)
97 (X := X) ψ delta hdelta)
98 hcontinuous hleft hright
99 simpa using hunique
101omit [DecidableEq X] in
102/-- Extensionality for continuous completed crossed differentials on a free pro-`C` source.
104The continuity hypotheses are put on the associated semidirect homomorphisms, which is the form
105used by the completed Fox construction before the target topology is fully structural. -/
107 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
108 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
109 (ψ : F →* H)
110 (delta epsilon :
111 F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
112 (hdelta :
113 IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
114 (hepsilon :
115 IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) epsilon)
116 (hdelta_continuous :
118 (X := X) ψ delta hdelta))
119 (hepsilon_continuous :
121 (X := X) ψ epsilon hepsilon))
122 (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
123 delta = epsilon := by
124 let f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
126 (X := X) ψ delta hdelta
127 let g : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
129 (X := X) ψ epsilon hepsilon
130 have hfg : ∀ x : X, f (ι x) = g (ι x) := by
131 intro x
132 apply ZCCompletedFoxSemidirect.ext
133 · exact hbasis x
134 · rfl
135 have hsemidirect : f = g := hι.hom_ext htarget hdelta_continuous hepsilon_continuous hfg
136 funext a
137 exact congrArg
138 (fun q : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => (q a).left)
139 hsemidirect
141/-- The coefficient homomorphism of a continuous completed crossed differential agrees with the
142right component of the canonical free pro-`C` semidirect lift. -/
144 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
145 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
146 (ψ : F →* H) (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
147 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
148 (hcontinuous :
150 (X := X) ψ delta hdelta))
151 (hbasis :
152 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
153 ψ =
155 (ProC := ProC) hι htarget (fun x : X => ψ (ι x))
157 (ProC := ProC) hι ψ delta hdelta hcontinuous hbasis) := by
158 apply MonoidHom.ext
159 intro g
160 have hgenerator :
161 ∀ x : X,
163 (X := X) ψ delta hdelta (ι x) =
164 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) (fun x : X => ψ (ι x)) x := by
165 intro x
166 apply ZCCompletedFoxSemidirect.ext
167 · exact hbasis x
168 · rfl
169 have hsemidirect := hι.lift_unique htarget
170 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) (fun x : X => ψ (ι x)))
172 (ProC := ProC) hι ψ delta hdelta hcontinuous hbasis)
174 (X := X) ψ delta hdelta)
175 hcontinuous hgenerator
176 simpa [freeProCZCCompletedFoxRightHom] using
177 congrArg (fun f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => (f g).right) hsemidirect
179/-- Existence and uniqueness of the free pro-`C` completed Fox derivative vector, formulated as
182 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
183 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
184 (φ : X → H)
185 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
186 ∃! delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
187 ∃ f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
188 Continuous f ∧
189 (∀ g : F, delta g = (f g).left) ∧
190 (∀ x : X, (f (ι x)).left =
191 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
192 ∀ x : X, (f (ι x)).right = φ x := by
194 (ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
195 · refine ⟨freeProCZCCompletedFoxSemidirectLift
196 (ProC := ProC) hι htarget φ hφ, ?_, ?_, ?_, ?_⟩
198 (ProC := ProC) hι htarget φ hφ
199 · intro g
200 rfl
202 (ProC := ProC) hι htarget φ hφ
204 (ProC := ProC) hι htarget φ hφ
205 · intro delta hdelta
206 rcases hdelta with ⟨f, hf, hdelta_left, hleft, hright⟩
207 have hgenerator :
208 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
209 intro x
210 apply ZCCompletedFoxSemidirect.ext
211 · exact hleft x
212 · exact hright x
213 have hf_eq := hι.lift_unique htarget
214 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ hf hgenerator
215 funext g
216 calc
217 delta g = (f g).left := hdelta_left g
219 (ProC := ProC) hι htarget φ hφ g).left := by
220 rw [hf_eq]
221 rfl
223 (ProC := ProC) hι htarget φ hφ g := rfl
226end
228end FoxDifferential