Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.Free.CanonicalFormula
ProCGroups/FoxDifferential/Completed/Continuous/Free/CanonicalFormula/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.Free.CanonicalFormula

1import ProCGroups.FoxDifferential.Completed.Continuous.Free.SourceFormula
3/-!
4# Fox differential: completed — continuous — free — canonical formula
6The principal declarations in this module are:
8- `freeProCZCCompletedFoxDerivativeVector_boundary`
9 Boundary-map form of the source-shaped completed Fox formula for the canonical free pro-\(C\)
10 semidirect lift.
11- `freeProCZCCompletedFoxDerivative_fundamental_formula`
12 Source-shaped completed Fox fundamental formula for the canonical free pro-\(C\) semidirect lift.
13- `freeProCZCCompletedFoxDerivative_euler_formula`
14 Explicit \([\rho g] - 1\) form of the source-shaped completed Fox-Euler formula for the canonical
15 free pro-\(C\) semidirect lift.
16-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
24universe u
27variable {C : ProCGroups.FiniteGroupClass.{u}}
28variable (X H : Type u) [DecidableEq X]
29variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32variable {F : Type u}
33variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
34variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
35variable [TopologicalSpace X]
37variable [DiscreteTopology X]
39section CanonicalSourceFormula
41variable [Fintype X]
42variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
43variable [T2Space (ZCCompletedFoxSemidirect C X H)]
44variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
45variable [CompactSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
46variable [T2Space (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
47variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
49/--
50Boundary-map form of the source-shaped completed Fox formula for the canonical free pro-\(C\)
51semidirect lift.
52-/
53theorem freeProCZCCompletedFoxDerivativeVector_boundary
54 {ι : X → F}
56 (htarget :
57 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
58 (htargetUnit :
59 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C PUnit H))
60 (φ : X → H) (g : F) :
61 freeProCZCCompletedFoxBoundary C φ
62 (freeProCZCCompletedFoxDerivativeVector
63 (C := C) hι htarget φ
64 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) =
65 zcCompletedGroupAlgebraBoundary C
66 (freeProCZCCompletedFoxRightHom
67 (C := C) hι htarget φ
68 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) g := by
69 let hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) :=
70 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ
71 simpa [freeProCZCCompletedFoxBoundary] using
72 freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential
73 (C := C) X H hι htargetUnit
74 (freeProCZCCompletedFoxRightHom
75 (C := C) hι htarget φ hφ)
76 (freeProCZCCompletedFoxDerivativeVector
77 (C := C) hι htarget φ hφ)
78 (continuous_freeProCZCCompletedFoxDerivativeVector
79 (C := C) X H hι htarget φ hφ)
80 (continuous_freeProCZCCompletedFoxRightHom
81 (C := C) X H hι htarget φ hφ)
82 (freeProCZCCompletedFoxDerivativeVector_generator
83 (C := C) hι htarget φ hφ)
84 g
86/--
87Source-shaped completed Fox fundamental formula for the canonical free pro-\(C\) semidirect
88lift.
89-/
90theorem freeProCZCCompletedFoxDerivative_fundamental_formula
91 {ι : X → F}
93 (htarget :
94 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
95 (htargetUnit :
96 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C PUnit H))
97 (φ : X → H) (g : F) :
98 zcCompletedGroupAlgebraBoundary C
99 (freeProCZCCompletedFoxRightHom
100 (C := C) hι htarget φ
101 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) g =
102 ∑ x : X,
103 freeProCZCCompletedFoxDerivativeVector
104 (C := C) hι htarget φ
105 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g x *
106 (zcGroupLike C H (φ x) - 1) := by
107 simpa [freeProCZCCompletedFoxBoundary_apply] using
108 (freeProCZCCompletedFoxDerivativeVector_boundary
109 (C := C) X H hι htarget htargetUnit φ g).symm
111/--
112Explicit \([\rho g] - 1\) form of the source-shaped completed Fox-Euler formula for the
113canonical free pro-\(C\) semidirect lift.
114-/
115theorem freeProCZCCompletedFoxDerivative_euler_formula
116 {ι : X → F}
118 (htarget :
119 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
120 (htargetUnit :
121 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C PUnit H))
122 (φ : X → H) (g : F) :
123 zcGroupLike C H
124 (freeProCZCCompletedFoxRightHom
125 (C := C) hι htarget φ
126 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) - 1 =
127 ∑ x : X,
128 freeProCZCCompletedFoxDerivativeVector
129 (C := C) hι htarget φ
130 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g x *
131 (zcGroupLike C H (φ x) - 1) := by
132 convert
133 freeProCZCCompletedFoxDerivative_fundamental_formula
134 (C := C) X H hι htarget htargetUnit φ g
135 using 1
136 rfl
138end CanonicalSourceFormula
142end
144end FoxDifferential