FoxDifferential/Completed/FreeProC/Uniqueness/Morphism.lean
1import FoxDifferential.Completed.FreeProC.SemidirectLift
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FreeProC/Uniqueness/Morphism.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/-- Categorical completed Fox semidirect morphisms from a free pro-`C` source are unique once
37 [ProCGroups.ProC.ProCGroup ProC F]
38 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
39 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
40 (φ : X → H)
41 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
42 (f :
43 ProCGrp.of ProC F ⟶
44 ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
45 (hgenerator :
46 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x) :
48 (ProC := ProC) hι φ hφ :=
49 hι.liftMorphism_unique
50 (ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
51 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ
52 (f := f) hgenerator
54/-- Componentwise uniqueness for categorical completed Fox semidirect morphisms from a free
55pro-`C` source. -/
57 [ProCGroups.ProC.ProCGroup ProC F]
58 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
59 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
60 (φ : X → H)
61 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
62 (f :
63 ProCGrp.of ProC F ⟶
64 ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
65 (hleft :
66 ∀ x : X, (f (ι x)).left =
67 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
68 (hright : ∀ x : X, (f (ι x)).right = φ x) :
70 (ProC := ProC) hι φ hφ := by
72 (ProC := ProC) hι φ hφ f
73 intro x
74 apply ZCCompletedFoxSemidirect.ext
75 · exact hleft x
76 · exact hright x
78/-- Existence and uniqueness of the categorical completed Fox semidirect morphism from a free
79pro-`C` source. -/
81 [ProCGroups.ProC.ProCGroup ProC F]
82 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
83 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
84 (φ : X → H)
85 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
86 ∃! f :
87 ProCGrp.of ProC F ⟶
88 ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
89 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
91 (ProC := ProC) hι φ hφ, ?_, ?_⟩
93 (ProC := ProC) hι φ hφ
94 · intro f hf
96 (ProC := ProC) hι φ hφ f hf
98/-- Componentwise existence and uniqueness of the categorical completed Fox semidirect morphism
99from a free pro-`C` source. -/
101 [ProCGroups.ProC.ProCGroup ProC F]
102 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
103 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
104 (φ : X → H)
105 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
106 ∃! f :
107 ProCGrp.of ProC F ⟶
108 ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
109 (∀ x : X, (f (ι x)).left =
110 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
111 ∀ x : X, (f (ι x)).right = φ x := by
113 (ProC := ProC) hι φ hφ, ?_, ?_⟩
114 · exact ⟨
116 (ProC := ProC) hι φ hφ,
118 (ProC := ProC) hι φ hφ⟩
119 · intro f hf
121 (ProC := ProC) hι φ hφ f hf.1 hf.2
123/-- Existence and uniqueness of the free pro-`C` completed Fox derivative vector, formulated as
125data. -/
127 [ProCGroups.ProC.ProCGroup ProC F]
128 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
129 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
130 (φ : X → H)
131 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
132 ∃! delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
133 ∃ f :
134 ProCGrp.of ProC F ⟶
135 ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
136 (∀ g : F, delta g = (f g).left) ∧
137 (∀ x : X, (f (ι x)).left =
138 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
139 ∀ x : X, (f (ι x)).right = φ x := by
141 (ProC := ProC) hι
142 (inferInstanceAs
143 (ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
144 φ hφ, ?_, ?_⟩
146 (ProC := ProC) hι φ hφ, ?_, ?_, ?_⟩
147 · intro g
148 rfl
150 (ProC := ProC) hι φ hφ
152 (ProC := ProC) hι φ hφ
153 · intro delta hdelta
154 rcases hdelta with ⟨f, hdelta_left, hleft, hright⟩
156 (ProC := ProC) hι φ hφ f hleft hright
157 funext g
158 calc
159 delta g = (f g).left := hdelta_left g
161 (ProC := ProC) hι φ hφ g).left := by
162 rw [hf_eq]
164 (ProC := ProC) hι
165 (inferInstanceAs
166 (ProCGroups.ProC.ProCGroup ProC
167 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
168 φ hφ g := rfl
171end
173end FoxDifferential