FoxDifferential/Completed/ProCIntegerCoefficients/FreeGroup/Fundamental.lean
1import FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Coordinates
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/FreeGroup/Fundamental.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed group algebra coefficients
14This module gives the free-group formulas for pro-\(C\) integer coefficients, used to compare completed Fox derivatives with ordinary finite-stage derivatives.
15-/
16namespace FoxDifferential
18noncomputable section
20open scoped BigOperators
22universe u v
25variable (C : ProCGroups.FiniteGroupClass.{v})
26variable {X : Type u} [DecidableEq X]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29section FiniteBasis
31variable [Fintype X]
33/-- Boundary-map form of the completed Fox fundamental formula. -/
35 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
36 zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w) =
37 zcCompletedGroupAlgebraBoundary C ψ w := by
38 let beta : FreeGroup X → ZCCompletedGroupAlgebra C H :=
39 fun w => zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w)
40 have hbeta :
41 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) beta :=
42 IsCrossedDifferential.map_linear
44 (zcFreeGroupFoxBoundary C ψ)
45 have hbasis :
46 ∀ x : X, beta (FreeGroup.of x) =
47 zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x) := by
48 intro x
49 simp only [zcFreeGroupFoxDerivativeVector_of, zcFreeGroupFoxBoundary_single, beta]
50 have hbeta_eq :
51 beta =
53 (A := ZCCompletedGroupAlgebra C H)
55 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x)) := by
57 (A := ZCCompletedGroupAlgebra C H)
59 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x))
60 beta hbeta hbasis
61 have hboundary_eq :
64 (A := ZCCompletedGroupAlgebra C H)
66 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x)) := by
68 (A := ZCCompletedGroupAlgebra C H)
70 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x))
73 (by intro x; rfl)
74 exact congrFun (hbeta_eq.trans hboundary_eq.symm) w
76/-- Conditional completed Fox boundary formula. Any completed crossed differential on a free
77group with the standard basis values satisfies the completed Fox boundary formula. -/
79 (ψ : FreeGroup X →* H)
80 (delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H))
81 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
82 (hbasis :
83 ∀ x : X, delta (FreeGroup.of x) =
84 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
85 (w : FreeGroup X) :
86 zcFreeGroupFoxBoundary C ψ (delta w) =
87 zcCompletedGroupAlgebraBoundary C ψ w := by
88 have hdelta_eq :
89 delta = zcFreeGroupFoxDerivativeVector C ψ :=
90 zcFreeGroupFoxDerivativeVector_unique C ψ delta hdelta hbasis
91 rw [hdelta_eq]
92 exact zcFreeGroupFoxBoundary_derivativeVector C ψ w
94/-- Conditional completed Fox fundamental formula. The finite Fox-Euler sum computed from any
95completed crossed differential with standard basis values is `[ψ(w)] - 1`. -/
97 (ψ : FreeGroup X →* H)
98 (delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H))
99 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
100 (hbasis :
101 ∀ x : X, delta (FreeGroup.of x) =
102 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
103 (w : FreeGroup X) :
104 zcCompletedGroupAlgebraBoundary C ψ w =
105 ∑ i : X,
106 delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
107 simpa [zcFreeGroupFoxBoundary_apply] using
108 (zcFreeGroupFoxBoundary_of_crossedDifferential C ψ delta hdelta hbasis w).symm
110/-- Explicit `[ψ(w)] - 1` form of the conditional completed Fox-Euler formula. -/
112 (ψ : FreeGroup X →* H)
113 (delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H))
114 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
115 (hbasis :
116 ∀ x : X, delta (FreeGroup.of x) =
117 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
118 (w : FreeGroup X) :
119 zcGroupLike C H (ψ w) - 1 =
120 ∑ i : X,
121 delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
122 simpa [zcCompletedGroupAlgebraBoundary] using
124 C ψ delta hdelta hbasis w
126/-- Completed Fox fundamental formula, also known as the completed Fox-Euler formula:
127`[ψ(w)] - 1 = ∑ i, (∂w/∂x_i) ([ψ(x_i)] - 1)`. -/
129 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
130 zcCompletedGroupAlgebraBoundary C ψ w =
131 ∑ i : X,
132 zcFreeGroupFoxDerivative C ψ i w *
133 (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
134 simpa [zcFreeGroupFoxBoundary_apply, zcFreeGroupFoxDerivative] using
135 (zcFreeGroupFoxBoundary_derivativeVector C ψ w).symm
137/-- Explicit `[ψ(w)] - 1` form of the completed Fox-Euler formula. -/
139 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
140 zcGroupLike C H (ψ w) - 1 =
141 ∑ i : X,
142 zcFreeGroupFoxDerivative C ψ i w *
143 (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
144 simpa [zcCompletedGroupAlgebraBoundary] using
148end FiniteBasis
151end
153end FoxDifferential