FoxDifferential.Completed.Comparison.SourceProjection
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem freeProCZCCompletedFoxBoundary_finiteStageProjection
(φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
(j : ZCCompletedGroupAlgebraIndex C H) :
zcCompletedGroupAlgebraProjection C H j
(freeProCZCCompletedFoxBoundary C φ v) =
∑ x : X,
zcCompletedGroupAlgebraProjection C H j (v x) *
zcCompletedGroupAlgebraProjection C H j (zcGroupLike C H (φ x) - 1)The finite-stage projection of the source-shaped completed Fox boundary map.
Show proof
by
rw [freeProCZCCompletedFoxBoundary_apply, zcCompletedGroupAlgebraProjection_sum]
apply Finset.sum_congr rfl
intro x _
simp only [zcCompletedGroupAlgebraProjection, zcCompletedGroupAlgebraProjection_mul,
zcCompletedGroupAlgebraProjection_sub, zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply,
zcCompletedGroupAlgebraProjection_one]Proof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxBoundary_finiteStageProjection_stage
(φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
(j : ZCCompletedGroupAlgebraIndex C H) :
zcCompletedGroupAlgebraProjection C H j
(freeProCZCCompletedFoxBoundary C φ v) =
∑ x : X,
zcCompletedGroupAlgebraProjection C H j (v x) *
(MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C j.2)
(QuotientGroup.mk (φ x)) - 1)Show proof
by
simpa [zcCompletedGroupAlgebraProjection] using
freeProCZCCompletedFoxBoundary_finiteStageProjection
(C := C) (X := X) (H := H) φ v jProof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem zcFreeFoxCoordinatesMap_finiteStageProjection
(η : H →ₜ* K)
(v : ZCFreeFoxCoordinates C (X := X) (H := H))
(j : ZCCompletedGroupAlgebraIndex C K) (x : X) :
zcCompletedGroupAlgebraProjection C K j
(zcFreeFoxCoordinatesMap (X := X) C hC η v x) =
zcCompletedGroupAlgebraMapStage C hC η j
(zcCompletedGroupAlgebraProjection C H
(j.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC η j.2) (v x))Componentwise finite-stage projection formula for target maps on completed Fox coordinates.
Show proof
by
simp only [zcFreeFoxCoordinatesMap, zcCompletedGroupAlgebraProjection_map]Proof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage
(η : H →ₜ* K) (φ : X → H)
(v : ZCFreeFoxCoordinates C (X := X) (H := H))
(j : ZCCompletedGroupAlgebraIndex C K) :
zcCompletedGroupAlgebraProjection C K j
(zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v)) =
∑ x : X,
zcCompletedGroupAlgebraMapStage C hC η j
(zcCompletedGroupAlgebraProjection C H
(j.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC η j.2) (v x)) *
(MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
(CompletedGroupAlgebraQuotientInClass K C j.2)
(QuotientGroup.mk (η (φ x))) - 1)The finite-stage projection of target naturality for source-shaped completed Fox boundary maps.
Show proof
by
rw [freeProCZCCompletedFoxBoundary_mapTarget]
rw [freeProCZCCompletedFoxBoundary_finiteStageProjection_stage]
apply Finset.sum_congr rfl
intro x _
rw [zcFreeFoxCoordinatesMap_finiteStageProjection]Proof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□