FoxDifferential.Completed.Continuous.Free.Rules
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
def freeProCZCCompletedFoxRightHomContinuousMonoidHom : F →ₜ* H where
toMonoidHom := freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ
continuous_toFun :=
continuous_freeProCZCCompletedFoxRightHom (ProC := ProC) X H hι htarget φ hφThe right component of the completed free pro-\(C\) Fox lift is bundled as a continuous homomorphism.
theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom :
(freeProCZCCompletedFoxRightHomContinuousMonoidHom
(ProC := ProC) hι htarget φ hφ).toMonoidHom =
freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφThe bundled right homomorphism has the expected underlying monoid homomorphism.
Show proof
rflProof. 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 freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply (g : F) :
freeProCZCCompletedFoxRightHomContinuousMonoidHom
(ProC := ProC) hι htarget φ hφ g =
freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ gEvaluation of the bundled right homomorphism.
Show proof
rflProof. 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. 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. 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 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 freeProCZCCompletedFoxRightHomContinuousMonoidHom_generator (x : X) :
freeProCZCCompletedFoxRightHomContinuousMonoidHom
(ProC := ProC) hι htarget φ hφ (ι x) = φ xThe bundled right homomorphism has the prescribed generator values.
Show proof
by
exact freeProCZCCompletedFoxRightHom_generator (ProC := ProC) hι htarget φ hφ xProof. 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.
□def freeProCZCCompletedFoxDerivativeVectorContinuousMap :
ContinuousMap F (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) where
toFun := freeProCZCCompletedFoxDerivativeVector (ProC := ProC) hι htarget φ hφ
continuous_toFun :=
continuous_freeProCZCCompletedFoxDerivativeVector (ProC := ProC) X H hι htarget φ hφThe completed free pro-\(C\) Fox derivative vector is bundled as a continuous map; it is a crossed differential, not a homomorphism.
theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_apply (g : F) :
freeProCZCCompletedFoxDerivativeVectorContinuousMap
(ProC := ProC) hι htarget φ hφ g =
freeProCZCCompletedFoxDerivativeVector (ProC := ProC) hι htarget φ hφ gEvaluation of the bundled continuous completed Fox derivative vector.
Show proof
rflProof. 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. 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 freeProCZCCompletedFoxDerivativeVectorContinuousMap_generator (x : X) :
freeProCZCCompletedFoxDerivativeVectorContinuousMap
(ProC := ProC) hι htarget φ hφ (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The bundled continuous completed Fox derivative vector has the prescribed generator values.
Show proof
by
simp only [freeProCZCCompletedFoxDerivativeVectorContinuousMap, ContinuousMap.coe_mk,
freeProCZCCompletedFoxDerivativeVector_generator]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\). 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 freeProCZCCompletedFoxDerivativeVectorContinuousMap_isCrossedDifferential :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ))
(freeProCZCCompletedFoxDerivativeVectorContinuousMap
(ProC := ProC) hι htarget φ hφ)The bundled continuous completed Fox derivative is a crossed differential.
Show proof
by
exact freeProCZCCompletedFoxDerivativeVector_isCrossedDifferential
(ProC := ProC) hι htarget φ hφ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. 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. 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 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 zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
((freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ).comp
(FreeGroup.lift ι)) w =
freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ ((FreeGroup.lift ι) w)Restricting the continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
Show proof
by
let ρ : F →* H :=
freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ
let D : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
freeProCZCCompletedFoxDerivativeVector (ProC := ProC) hι htarget φ hφ
let δ : FreeGroup X →
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
fun w => D ((FreeGroup.lift ι) w)
have hδ :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι))) δ := by
intro u v
simpa [δ, ρ, D, map_mul, MonoidHom.comp_apply] using
freeProCZCCompletedFoxDerivativeVector_isCrossedDifferential
(ProC := ProC) hι htarget φ hφ ((FreeGroup.lift ι) u) ((FreeGroup.lift ι) v)
have hbasis :
∀ x : X, δ (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
intro x
simp only [FreeGroup.lift_apply_of, freeProCZCCompletedFoxDerivativeVector_generator, δ, D]
have hδeq :
δ =
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(ρ.comp (FreeGroup.lift ι)) :=
zcFreeGroupFoxDerivativeVector_unique
ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι)) δ hδ hbasis
exact congrFun hδeq w |>.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. 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. 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 zcFreeFoxDerivVec_eq_freeProCCompletedFoxDerivVec_comp_lift_mapTarget
(hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(η : H →ₜ* K) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(η.toMonoidHom.comp
((freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ).comp
(FreeGroup.lift ι))) w =
zcFreeFoxCoordinatesMap (X := X) ProC.finiteQuotientClass hC η
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ ((FreeGroup.lift ι) w))Source restriction and target naturality for the continuous completed Fox derivative.
Show proof
by
rw [zcFreeGroupFoxDerivativeVector_mapTarget]
rw [zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
(ProC := ProC) hι htarget φ hφ w]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\). 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. 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. 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 zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
((freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen).comp
(FreeGroup.lift ι)) w =
freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w)Restricting the converging-set continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
Show proof
by
let ρ : F →* H :=
freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen
let D : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen
let δ : FreeGroup X →
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
fun w => D ((FreeGroup.lift ι) w)
have hδ :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι))) δ := by
intro u v
simpa [δ, ρ, D, map_mul, MonoidHom.comp_apply] using
freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_isCrossedDifferential
(ProC := ProC) hι htarget φ hφconv hφgen
((FreeGroup.lift ι) u) ((FreeGroup.lift ι) v)
have hbasis :
∀ x : X, δ (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
intro x
simp only [FreeGroup.lift_apply_of, freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator, δ, D]
have hδeq :
δ =
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(ρ.comp (FreeGroup.lift ι)) :=
zcFreeGroupFoxDerivativeVector_unique
ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι)) δ hδ hbasis
exact congrFun hδeq w |>.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. 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. 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 zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift_mapTarget
(hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(η : H →ₜ* K) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(η.toMonoidHom.comp
((freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen).comp
(FreeGroup.lift ι))) w =
zcFreeFoxCoordinatesMap (X := X) ProC.finiteQuotientClass hC η
(freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w))Source restriction and target naturality for the converging-set continuous completed Fox derivative.
Show proof
by
rw [zcFreeGroupFoxDerivativeVector_mapTarget]
rw [zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
(ProC := ProC) hι htarget φ hφconv hφgen w]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\). 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. 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. 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 zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
((freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv).comp
(FreeGroup.lift ι)) w =
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv ((FreeGroup.lift ι) w)Restricting the closed-generated continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
Show proof
by
let ρ : F →* H :=
freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv
let D : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv
let δ : FreeGroup X →
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
fun w => D ((FreeGroup.lift ι) w)
have hδ :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι))) δ := by
intro u v
simpa [δ, ρ, D, map_mul, MonoidHom.comp_apply] using
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_isCrossedDifferential
(ProC := ProC) hι φ htarget hφconv
((FreeGroup.lift ι) u) ((FreeGroup.lift ι) v)
have hbasis :
∀ x : X, δ (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
intro x
simp only [FreeGroup.lift_apply_of, freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator, δ, D]
have hδeq :
δ =
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(ρ.comp (FreeGroup.lift ι)) :=
zcFreeGroupFoxDerivativeVector_unique
ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι)) δ hδ hbasis
exact congrFun hδeq w |>.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. 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. 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 zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift_mapTarget
(hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(η : H →ₜ* K) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(η.toMonoidHom.comp
((freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv).comp
(FreeGroup.lift ι))) w =
zcFreeFoxCoordinatesMap (X := X) ProC.finiteQuotientClass hC η
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv ((FreeGroup.lift ι) w))Source restriction and target naturality for the closed-generated continuous completed Fox derivative.
Show proof
by
rw [zcFreeGroupFoxDerivativeVector_mapTarget]
rw [zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
(ProC := ProC) hι φ htarget hφconv w]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\). 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. 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. 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.
□