theorem freeProCZCCompletedFoxDerivativeVector_boundary
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htarget :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(htargetUnit :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
(φ : X → H) (g : F) :
freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass φ
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProC) X H φ) g) =
zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHom
(ProC := ProC) hι htarget φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProC) X H φ)) gBoundary-map form of the source-shaped completed Fox formula for the canonical free pro-\(C\) semidirect lift.
Show proof
by
let hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) :=
continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X H φ
simpa [freeProCZCCompletedFoxBoundary] using
freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential
(ProC := ProC) X H hι htargetUnit
(freeProCZCCompletedFoxRightHom
(ProC := ProC) hι htarget φ hφ)
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ)
(freeProCZCCompletedFoxDerivativeVector_isCrossedDifferential
(ProC := ProC) hι htarget φ hφ)
(continuous_freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) X H hι htarget φ hφ)
(continuous_freeProCZCCompletedFoxRightHom
(ProC := ProC) X H hι htarget φ hφ)
(freeProCZCCompletedFoxDerivativeVector_generator
(ProC := ProC) hι htarget φ hφ)
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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxDerivative_fundamental_formula
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htarget :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(htargetUnit :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
(φ : X → H) (g : F) :
zcCompletedGroupAlgebraBoundary ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHom
(ProC := ProC) hι htarget φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProC) X H φ)) g =
∑ x : X,
freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProC) X H φ) g x *
(zcGroupLike ProC.finiteQuotientClass H (φ x) - 1)Source-shaped completed Fox fundamental formula for the canonical free pro-\(C\) semidirect lift.
Show proof
by
simpa [freeProCZCCompletedFoxBoundary_apply] using
(freeProCZCCompletedFoxDerivativeVector_boundary
(ProC := ProC) X H hι htarget htargetUnit φ 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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxDerivative_euler_formula
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htarget :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(htargetUnit :
ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass PUnit H))
(φ : X → H) (g : F) :
zcGroupLike ProC.finiteQuotientClass H
(freeProCZCCompletedFoxRightHom
(ProC := ProC) hι htarget φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProC) X H φ) g) - 1 =
∑ x : X,
freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProC) X H φ) g x *
(zcGroupLike ProC.finiteQuotientClass H (φ x) - 1)Explicit \([\rho g] - 1\) form of the source-shaped completed Fox-Euler formula for the canonical free pro-\(C\) semidirect lift.
Show proof
by
simpa [zcCompletedGroupAlgebraBoundary] using
freeProCZCCompletedFoxDerivative_fundamental_formula
(ProC := ProC) X H hι htarget htargetUnit φ 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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□