FoxDifferential/Completed/Continuous/Free/SourceFormula.lean

1import FoxDifferential.Completed.Continuous.Free.Continuity

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/FoxDifferential/Completed/Continuous/Free/SourceFormula.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]

35section SourceFormula

37variable [Fintype X]

39omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in

40/-- Source-shaped completed Fox boundary formula for continuous crossed differentials out of an

41free pro-`C` source. -/

42theorem freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential

43 {ι : X → F}

44 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)

45 (htargetUnit :

46 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))

47 (ψ : F →* H)

48 (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))

49 (hdelta : IsCrossedDifferential

50 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)

51 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)

52 (hbasis :

53 ∀ x : X, delta (ι x) =

54 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))

55 (g : F) :

56 freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass (fun x : X => ψ (ι x))

57 (delta g) =

58 zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ g := by

59 let beta : F → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H :=

60 fun g => freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass

61 (fun x : X => ψ (ι x)) (delta g)

62 have hbeta :

63 IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ)

64 beta := by

65 exact IsCrossedDifferential.map_linear hdelta

66 (freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass (fun x : X => ψ (ι x)))

67 let betaVec : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass

68 (X := PUnit) (H := H) :=

69 fun g _ => beta g

70 have hbetaVec :

71 IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ)

72 betaVec := by

73 intro g h

74 funext u

75 exact hbeta g h

76 let boundaryVec : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass

77 (X := PUnit) (H := H) :=

78 fun g _ => zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ g

79 have hboundaryVec :

80 IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ)

81 boundaryVec := by

82 intro g h

83 funext u

84 exact zcCompletedGroupAlgebraBoundary_isCrossedDifferential

85 ProC.finiteQuotientClass ψ g h

86 have hbeta_continuous : Continuous beta := by

87 exact (continuous_freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass

88 (fun x : X => ψ (ι x))).comp hdelta_continuous

89 have hbetaVec_continuous : Continuous betaVec := by

90 exact continuous_pi fun _ => hbeta_continuous

91 have hboundary_continuous :

92 Continuous (zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ) :=

93 continuous_zcCompletedGroupAlgebraBoundary

94 (C := ProC.finiteQuotientClass) (G := H) ψ hψ_continuous

95 have hboundaryVec_continuous : Continuous boundaryVec := by

96 exact continuous_pi fun _ => hboundary_continuous

97 let f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H :=

98 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential

99 (ProC := ProC) (X := PUnit) (F := F) (H := H) ψ betaVec hbetaVec

100 let h : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H :=

101 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential

102 (ProC := ProC) (X := PUnit) (F := F) (H := H) ψ boundaryVec hboundaryVec

103 have hf_continuous : Continuous f :=

104 continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential

105 (ProC := ProC) (X := PUnit) (F := F) (H := H)

106 ψ betaVec hbetaVec hbetaVec_continuous hψ_continuous

107 have hh_continuous : Continuous h :=

108 continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential

109 (ProC := ProC) (X := PUnit) (F := F) (H := H) ψ boundaryVec hboundaryVec

110 hboundaryVec_continuous hψ_continuous

111 have hgen : ∀ x : X, f (ι x) = h (ι x) := by

112 intro x

113 apply ZCCompletedFoxSemidirect.ext

114 · funext u

115 simp only [freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left, hbasis x,

116 freeProCZCCompletedFoxBoundary_single, zcCompletedGroupAlgebraBoundary, f, betaVec, beta, h, boundaryVec]

117 · rfl

118 have hfh : f = h := hι.hom_ext htargetUnit hf_continuous hh_continuous hgen

119 have hleft := congrArg

120 (fun q : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H =>

121 (q g).left PUnit.unit) hfh

122 simpa [f, h, betaVec, boundaryVec, beta] using hleft

123

124omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in

125/-- Source-shaped completed Fox fundamental formula for continuous crossed differentials out of

126free pro-`C` source. -/

127theorem freeProCZCCompletedFoxDerivative_fundFormula_of_continuousCrossedDiff

128 {ι : X → F}

129 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)

130 (htargetUnit :

131 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))

132 (ψ : F →* H)

133 (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))

134 (hdelta : IsCrossedDifferential

135 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)

136 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)

137 (hbasis :

138 ∀ x : X, delta (ι x) =

139 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))

140 (g : F) :

141 zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ g =

142 ∑ x : X, delta g x *

143 (zcGroupLike ProC.finiteQuotientClass H (ψ (ι x)) - 1) := by

144 simpa [freeProCZCCompletedFoxBoundary_apply] using

145 (freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential

146 (ProC := ProC) X H hι htargetUnit ψ delta hdelta hdelta_continuous hψ_continuous

147 hbasis g).symm

148

149omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in

150/-- Explicit `[ψ g] - 1` form of the source-shaped completed Fox-Euler formula for continuous

151crossed differentials out of a free pro-`C` source. -/

152theorem freeProCZCCompletedFoxDerivative_euler_formula_of_continuousCrossedDifferential

153 {ι : X → F}

154 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)

155 (htargetUnit :

156 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))

157 (ψ : F →* H)

158 (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))

159 (hdelta : IsCrossedDifferential

160 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)

161 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)

162 (hbasis :

163 ∀ x : X, delta (ι x) =

164 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))

165 (g : F) :

166 zcGroupLike ProC.finiteQuotientClass H (ψ g) - 1 =

167 ∑ x : X, delta g x *

168 (zcGroupLike ProC.finiteQuotientClass H (ψ (ι x)) - 1) := by

169 simpa [zcCompletedGroupAlgebraBoundary] using

170 freeProCZCCompletedFoxDerivative_fundFormula_of_continuousCrossedDiff

171 (ProC := ProC) X H hι htargetUnit ψ delta hdelta hdelta_continuous hψ_continuous hbasis g

173end SourceFormula

177end

179end FoxDifferential