FoxDifferential/Completed/FreeProC/Uniqueness/Lift.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/Lift.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/-- Continuous completed Fox semidirect lifts from a free pro-`C` source are unique once their
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 (hgenerator :
44 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x) :
46 (ProC := ProC) hι htarget φ hφ :=
47 hι.lift_unique htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
48 hφ hf hgenerator
50/-- Componentwise uniqueness for continuous completed Fox semidirect lifts from a free pro-`C`
51source. -/
53 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
54 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
55 (φ : X → H)
56 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
57 (f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
58 (hf : Continuous f)
59 (hleft :
60 ∀ x : X, (f (ι x)).left =
61 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
62 (hright : ∀ x : X, (f (ι x)).right = φ x) :
64 (ProC := ProC) hι htarget φ hφ := by
66 (ProC := ProC) hι htarget φ hφ f hf
67 intro x
68 apply ZCCompletedFoxSemidirect.ext
69 · exact hleft x
70 · exact hright x
72/-- Continuous completed Fox semidirect homomorphisms from a free pro-`C` source are unique once
75 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
76 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
77 (φ : X → H)
78 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
79 (f : F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
80 (hgenerator :
81 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x) :
83 (ProC := ProC) hι htarget φ hφ :=
84 hι.liftHom_unique htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
85 hφ hgenerator
87/-- Componentwise uniqueness for continuous completed Fox semidirect homomorphisms from a free
88pro-`C` source. -/
90 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
91 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
92 (φ : X → H)
93 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
94 (f : F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
95 (hleft :
96 ∀ x : X, (f (ι x)).left =
97 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
98 (hright : ∀ x : X, (f (ι x)).right = φ x) :
100 (ProC := ProC) hι htarget φ hφ := by
102 (ProC := ProC) hι htarget φ hφ f
103 intro x
104 apply ZCCompletedFoxSemidirect.ext
105 · exact hleft x
106 · exact hright x
108/-- Existence and uniqueness of the continuous completed Fox semidirect homomorphism from a free
109pro-`C` source. -/
111 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
112 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
113 (φ : X → H)
114 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
115 ∃! f : F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
116 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
118 (ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
120 (ProC := ProC) hι htarget φ hφ
121 · intro f hf
123 (ProC := ProC) hι htarget φ hφ f hf
125/-- Componentwise existence and uniqueness of the continuous completed Fox semidirect
126homomorphism from a free pro-`C` source. -/
128 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
129 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
130 (φ : X → H)
131 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
132 ∃! f : F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
133 (∀ x : X, (f (ι x)).left =
134 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
135 ∀ x : X, (f (ι x)).right = φ x := by
137 (ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
138 · exact ⟨
140 (ProC := ProC) hι htarget φ hφ,
142 (ProC := ProC) hι htarget φ hφ⟩
143 · intro f hf
145 (ProC := ProC) hι htarget φ hφ f hf.1 hf.2
148end
150end FoxDifferential