FoxDifferential/Completed/FreeProC/Uniqueness/Existence.lean
1import FoxDifferential.Completed.FreeProC.Uniqueness.Lift
2import FoxDifferential.Completed.FreeProC.Uniqueness.Morphism
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/FreeProC/Uniqueness/Existence.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Free pro-C completed Fox calculus
15Free pro-C sources are treated through completed Fox derivatives, stage projections, density arguments, and semidirect lift formulas.
16-/
17namespace FoxDifferential
19noncomputable section
21open ProCGroups.FreeProC
23universe u
26variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
27variable {X F H : Type u}
28variable [TopologicalSpace X]
29variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
30variable [DecidableEq X]
31variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
33variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
35/-- Existence and uniqueness of the free pro-`C` completed Fox derivative vector, formulated as
38 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
39 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
40 (φ : X → H)
41 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
42 ∃! delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
43 ∃ f : F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
44 (∀ g : F, delta g = (f g).left) ∧
45 (∀ x : X, (f (ι x)).left =
46 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
47 ∀ x : X, (f (ι x)).right = φ x := by
49 (ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
50 · refine ⟨freeProCZCCompletedFoxSemidirectLiftHom
51 (ProC := ProC) hι htarget φ hφ, ?_, ?_, ?_⟩
52 · intro g
53 rfl
55 (ProC := ProC) hι htarget φ hφ
57 (ProC := ProC) hι htarget φ hφ
58 · intro delta hdelta
59 rcases hdelta with ⟨f, hdelta_left, hleft, hright⟩
61 (ProC := ProC) hι htarget φ hφ f hleft hright
62 funext g
63 calc
64 delta g = (f g).left := hdelta_left g
66 (ProC := ProC) hι htarget φ hφ g).left := by
67 rw [hf_eq]
69 (ProC := ProC) hι htarget φ hφ g := rfl
71/-- Existence and uniqueness of the continuous completed Fox semidirect lift from a free pro-`C`
72source. -/
74 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
75 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
76 (φ : X → H)
77 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
78 ∃! f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
79 Continuous f ∧
80 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
81 hι.existsUnique_lift htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ
83/-- Componentwise existence and uniqueness of the continuous completed Fox semidirect lift from a
84free pro-`C` source. -/
86 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
87 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
88 (φ : X → H)
89 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
90 ∃! f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
91 Continuous f ∧
92 (∀ x : X, (f (ι x)).left =
93 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
94 ∀ x : X, (f (ι x)).right = φ x := by
96 (ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
97 · exact ⟨
99 (ProC := ProC) hι htarget φ hφ,
101 (ProC := ProC) hι htarget φ hφ,
103 (ProC := ProC) hι htarget φ hφ⟩
104 · intro f hf
106 (ProC := ProC) hι htarget φ hφ f hf.1 hf.2.1 hf.2.2
109end
111end FoxDifferential