FoxDifferential/Completed/Continuous/Free/CanonicalFormula.lean
1import FoxDifferential.Completed.Continuous.Free.SourceFormula
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/Free/CanonicalFormula.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Continuous crossed differentials
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open scoped BigOperators
22universe u
25variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
26variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
27variable (X H : Type u) [DecidableEq X]
28variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
31variable {F : Type u}
32variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
33variable [TopologicalSpace X]
35variable [DiscreteTopology X]
37section CanonicalSourceFormula
39variable [Fintype X]
41omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
42/-- Boundary-map form of the source-shaped completed Fox formula for the canonical free pro-`C`
43semidirect lift. -/
45 {ι : X → F}
46 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
47 (htarget :
48 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
49 (htargetUnit :
50 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
51 (φ : X → H) (g : F) :
52 freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass φ
54 (ProC := ProC) hι htarget φ
56 (ProC := ProC) X H φ) g) =
57 zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass
59 (ProC := ProC) hι htarget φ
61 (ProC := ProC) X H φ)) g := by
62 let hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) :=
63 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X H φ
64 simpa [freeProCZCCompletedFoxBoundary] using
66 (ProC := ProC) X H hι htargetUnit
68 (ProC := ProC) hι htarget φ hφ)
70 (ProC := ProC) hι htarget φ hφ)
72 (ProC := ProC) hι htarget φ hφ)
74 (ProC := ProC) X H hι htarget φ hφ)
76 (ProC := ProC) X H hι htarget φ hφ)
78 (ProC := ProC) hι htarget φ hφ)
79 g
81omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
82/-- Source-shaped completed Fox fundamental formula for the canonical free pro-`C`
83semidirect lift. -/
85 {ι : X → F}
86 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
87 (htarget :
88 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
89 (htargetUnit :
90 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
91 (φ : X → H) (g : F) :
92 zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass
94 (ProC := ProC) hι htarget φ
96 (ProC := ProC) X H φ)) g =
97 ∑ x : X,
99 (ProC := ProC) hι htarget φ
101 (ProC := ProC) X H φ) g x *
102 (zcGroupLike ProC.finiteQuotientClass H (φ x) - 1) := by
103 simpa [freeProCZCCompletedFoxBoundary_apply] using
105 (ProC := ProC) X H hι htarget htargetUnit φ g).symm
107omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
108/-- Explicit `[ρ g] - 1` form of the source-shaped completed Fox-Euler formula for the canonical
109free pro-`C` semidirect lift. -/
111 {ι : X → F}
112 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
113 (htarget :
114 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
115 (htargetUnit :
116 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
117 (φ : X → H) (g : F) :
118 zcGroupLike ProC.finiteQuotientClass H
120 (ProC := ProC) hι htarget φ
122 (ProC := ProC) X H φ) g) - 1 =
123 ∑ x : X,
125 (ProC := ProC) hι htarget φ
127 (ProC := ProC) X H φ) g x *
128 (zcGroupLike ProC.finiteQuotientClass H (φ x) - 1) := by
129 simpa [zcCompletedGroupAlgebraBoundary] using
131 (ProC := ProC) X H hι htarget htargetUnit φ g
133end CanonicalSourceFormula
137end
139end FoxDifferential