FoxDifferential.Completed.Continuous.Free.SourceFormula
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htargetUnit :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
(ψ : F →* H)
(delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
(g : F) :
freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass (fun x : X => ψ (ι x))
(delta g) =
zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ gSource-shaped completed Fox boundary formula for continuous crossed differentials out of a free pro-\(C\) source.
Show proof
by
let beta : F → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H :=
fun g => freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass
(fun x : X => ψ (ι x)) (delta g)
have hbeta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ)
beta := by
exact IsCrossedDifferential.map_linear hdelta
(freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass (fun x : X => ψ (ι x)))
let betaVec : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := PUnit) (H := H) :=
fun g _ => beta g
have hbetaVec :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ)
betaVec := by
intro g h
funext u
exact hbeta g h
let boundaryVec : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := PUnit) (H := H) :=
fun g _ => zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ g
have hboundaryVec :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ)
boundaryVec := by
intro g h
funext u
exact zcCompletedGroupAlgebraBoundary_isCrossedDifferential
ProC.finiteQuotientClass ψ g h
have hbeta_continuous : Continuous beta := by
exact (continuous_freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass
(fun x : X => ψ (ι x))).comp hdelta_continuous
have hbetaVec_continuous : Continuous betaVec := by
exact continuous_pi fun _ => hbeta_continuous
have hboundary_continuous :
Continuous (zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ) :=
continuous_zcCompletedGroupAlgebraBoundary
(C := ProC.finiteQuotientClass) (G := H) ψ hψ_continuous
have hboundaryVec_continuous : Continuous boundaryVec := by
exact continuous_pi fun _ => hboundary_continuous
let f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H :=
freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ProC := ProC) (X := PUnit) (F := F) (H := H) ψ betaVec hbetaVec
let h : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H :=
freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ProC := ProC) (X := PUnit) (F := F) (H := H) ψ boundaryVec hboundaryVec
have hf_continuous : Continuous f :=
continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ProC := ProC) (X := PUnit) (F := F) (H := H)
ψ betaVec hbetaVec hbetaVec_continuous hψ_continuous
have hh_continuous : Continuous h :=
continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ProC := ProC) (X := PUnit) (F := F) (H := H) ψ boundaryVec hboundaryVec
hboundaryVec_continuous hψ_continuous
have hgen : ∀ x : X, f (ι x) = h (ι x) := by
intro x
apply ZCCompletedFoxSemidirect.ext
· funext u
simp only [freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left, hbasis x,
freeProCZCCompletedFoxBoundary_single, zcCompletedGroupAlgebraBoundary, f, betaVec, beta, h, boundaryVec]
· rfl
have hfh : f = h := hι.hom_ext htargetUnit hf_continuous hh_continuous hgen
have hleft := congrArg
(fun q : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H =>
(q g).left PUnit.unit) hfh
simpa [f, h, betaVec, boundaryVec, beta] using hleftProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem freeProCZCCompletedFoxDerivative_fundFormula_of_continuousCrossedDiff
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htargetUnit :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
(ψ : F →* H)
(delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
(g : F) :
zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass ψ g =
∑ x : X, delta g x *
(zcGroupLike ProC.finiteQuotientClass H (ψ (ι x)) - 1)Source-shaped completed Fox fundamental formula for continuous crossed differentials out of free pro-\(C\) source.
Show proof
by
simpa [freeProCZCCompletedFoxBoundary_apply] using
(freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential
(ProC := ProC) X H hι htargetUnit ψ delta hdelta hdelta_continuous hψ_continuous
hbasis g).symmProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem freeProCZCCompletedFoxDerivative_euler_formula_of_continuousCrossedDifferential
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htargetUnit :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
(ψ : F →* H)
(delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
(g : F) :
zcGroupLike ProC.finiteQuotientClass H (ψ g) - 1 =
∑ x : X, delta g x *
(zcGroupLike ProC.finiteQuotientClass H (ψ (ι x)) - 1)Explicit \([\psi(g)] - 1\) form of the source-shaped completed Fox-Euler formula for continuous crossed differentials out of a free pro-\(C\) source.
Show proof
by
simpa [zcCompletedGroupAlgebraBoundary] using
freeProCZCCompletedFoxDerivative_fundFormula_of_continuousCrossedDiff
(ProC := ProC) X H hι htargetUnit ψ delta hdelta hdelta_continuous hψ_continuous hbasis gProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□