import
def zcCompletedDifferentialModuleUniversalTopology (ψ : G →* H) :
TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
TopologicalSpace.coinduced (zcUniversalDifferential C ψ) inferInstanceThe final topology on the completed universal differential module generated by the universal crossed differential \(G \to d_{\mathbb{Z}_C\llbracket H\rrbracket}G\). Unlike the finite-rank free-coordinate topology, this topology is available for an arbitrary source group and states the genuine topological universal property: a map out is continuous exactly when its composite with the universal differential is continuous.
theorem continuous_zcUniversalDifferential_universalTopology
(ψ : G →* H) :
@Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
(zcCompletedDifferentialModuleUniversalTopology C ψ)
(zcUniversalDifferential C ψ)The universal crossed differential is continuous for the final universal topology.
Show proof
continuous_coinduced_rngProof. 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 continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
{ψ : G →* H} {delta : G → A}
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
@Continuous (ZCCompletedDifferentialModule C ψ) A
(zcCompletedDifferentialModuleUniversalTopology C ψ) inferInstance
(zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) ↔
Continuous deltaThe completed differential-module criterion is equivalent to the corresponding finite-stage coordinate condition.
Show proof
by
rw [continuous_coinduced_dom]
have hcomp :
(zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) ∘
(zcUniversalDifferential C ψ) = delta := by
funext g
exact zcCompletedDifferentialModuleLift_universal
(A := A) C ψ delta hdelta g
rw [hcomp]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. Exactness is proved by identifying the image of the previous boundary map with the elements whose Fox coordinates vanish under the next boundary map, giving both inclusions at the finite stages. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□instance zcCompletedDifferentialModuleUniversalTopologyInst :
TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleUniversalTopology C ψThe completed differential module carries the universal finite-stage topology.
def zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
(delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcont : Continuous delta) :
ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
toLinearMap := zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta
cont :=
(continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
(C := C) (G := G) (H := H) (A := A) (ψ := ψ) (delta := delta) hdelta).2 hcontThe representing universal lift as a continuous linear map for the final universal topology, from a continuous crossed differential.
theorem zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap_apply
(delta : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcont : Continuous delta)
(m : ZCCompletedDifferentialModule C ψ) :
zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
(C := C) (G := G) (H := H) (A := A) ψ delta hdelta hcont m =
zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta mEvaluation of the universal-topology continuous lift.
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.
□def zcCompletedContinuousCrossedDifferentialEquivContinuousLinearMap :
{delta : G → A //
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧ Continuous delta} ≃
(ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where
toFun delta :=
zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
(C := C) (G := G) (H := H) (A := A) ψ delta.1 delta.2.1 delta.2.2
invFun f :=
⟨fun g => f (zcUniversalDifferential C ψ g), by
constructor
· intro g h
change f (zcUniversalDifferential C ψ (g * h)) =
f (zcUniversalDifferential C ψ g) +
zcCompletedGroupAlgebraScalar C ψ g •
f (zcUniversalDifferential C ψ h)
rw [zcUniversalDifferential_mul]
simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
· exact f.cont.comp (continuous_zcUniversalDifferential_universalTopology C ψ)⟩
left_inv delta := by
apply Subtype.ext
funext g
exact zcCompletedDifferentialModuleLift_universal
(A := A) C ψ delta.1 delta.2.1 g
right_inv f := by
apply ContinuousLinearMap.ext
intro m
have hdelta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ)
(fun g => f (zcUniversalDifferential C ψ g)) := by
intro g h
change f (zcUniversalDifferential C ψ (g * h)) =
f (zcUniversalDifferential C ψ g) +
zcCompletedGroupAlgebraScalar C ψ g •
f (zcUniversalDifferential C ψ h)
rw [zcUniversalDifferential_mul]
simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
have hlin :
f.toLinearMap =
zcCompletedDifferentialModuleLift (A := A) C ψ
(fun g => f (zcUniversalDifferential C ψ g)) hdelta := by
apply zcCompletedDifferentialModuleLift_unique (A := A) C ψ
intro g
rfl
exact congrFun (congrArg DFunLike.coe hlin.symm) mTopological universal representation theorem for completed crossed differentials. With the final universal topology on the completed differential module, continuous crossed differentials \(G \to A\) are equivalent to continuous \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear maps out of the completed universal differential module.
theorem continuous_zcToCompletedGroupAlgebra_universalTopology
(ψ : G →* H) (hψ : Continuous ψ) :
@Continuous (ZCCompletedDifferentialModule C ψ) (ZCCompletedGroupAlgebra C H)
(zcCompletedDifferentialModuleUniversalTopology C ψ) inferInstance
(zcToCompletedGroupAlgebra C ψ)The universal boundary map from the completed differential module to \(\mathbb{Z}_C\llbracket H\rrbracket\) is continuous for the final universal topology whenever the target homomorphism is continuous.
Show proof
by
exact
(continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
(C := C) (G := G) (H := H) (A := ZCCompletedGroupAlgebra C H)
(ψ := ψ) (delta := zcCompletedGroupAlgebraBoundary C ψ)
(zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ)).2
(continuous_zcCompletedGroupAlgebraBoundary (C := C) (G := H) ψ 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\). 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 zcCompletedDifferentialModuleFreeTopology (ψ : FreeGroup X →* H) :
TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
TopologicalSpace.induced (zcDifferentialToFreeFoxCoordinates C ψ) inferInstanceThe finite-rank topology on the completed universal module, induced by completed Fox coordinates. This is intentionally a named topology, not a global instance.
theorem continuous_zcDifferentialToFreeFoxCoordinates_freeTopology
(ψ : FreeGroup X →* H) :
@Continuous (ZCCompletedDifferentialModule C ψ)
(ZCFreeFoxCoordinates C (X := X) (H := H))
(zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
(zcDifferentialToFreeFoxCoordinates C ψ)The coordinate map out of the completed universal module is continuous for the finite-rank coordinate-induced topology.
Show proof
continuous_induced_domProof. 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 continuous_zcFreeFoxCoordinatesLinearMap_freeTopology
(ψ : FreeGroup X →* H) :
@Continuous (ZCFreeFoxCoordinates C (X := X) (H := H))
(ZCCompletedDifferentialModule C ψ) inferInstance
(zcCompletedDifferentialModuleFreeTopology C ψ)
(zcFreeFoxCoordinatesLinearMap C ψ)The coordinate-to-universal-module map is continuous for the finite-rank coordinate-induced topology.
Show proof
by
rw [continuous_induced_rng]
have hcomp :
(zcDifferentialToFreeFoxCoordinates C ψ) ∘
(zcFreeFoxCoordinatesLinearMap C ψ) =
id := by
funext v
exact congrFun
(congrArg DFunLike.coe
(zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap C ψ)) v
rw [hcomp]
exact continuous_idProof. 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.
□instance instContinuousSMulZCFreeFoxCoordinates :
ContinuousSMul (ZCCompletedGroupAlgebra C H)
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
inferInstanceScalar multiplication is continuous for the relevant inverse-limit topology.
instance instContinuousSMulZCCompletedDifferentialModuleFreeTopology
(ψ : FreeGroup X →* H) :
@ContinuousSMul (ZCCompletedGroupAlgebra C H)
(ZCCompletedDifferentialModule C ψ)
inferInstance inferInstance (zcCompletedDifferentialModuleFreeTopology C ψ) :=
ContinuousSMul.induced (zcDifferentialToFreeFoxCoordinates C ψ)Scalar multiplication is continuous for the relevant inverse-limit topology.
def zcFreeCrossedDifferentialCoordinateLift
(delta : FreeGroup X → A) :
ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H] A where
toFun v := ∑ x : X, v x • delta (FreeGroup.of x)
map_add' v w := by
simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
map_smul' r v := by
simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]theorem zcFreeCrossedDifferentialCoordinateLift_apply
(delta : FreeGroup X → A)
(v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcFreeCrossedDifferentialCoordinateLift (H := H) C delta v =
∑ x : X, v x • delta (FreeGroup.of x)Evaluation formula for the coordinate lift attached to generator values.
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. 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 zcFreeCrossedDifferentialCoordinateLift_derivativeVector
(ψ : FreeGroup X →* H) (delta : FreeGroup X → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(w : FreeGroup X) :
zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
(zcFreeGroupFoxDerivativeVector C ψ w) =
delta wThe coordinate lift applied to the completed free derivative vector recovers the crossed differential it represents.
Show proof
by
let L := zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
let beta : FreeGroup X → A := fun w => L (zcFreeGroupFoxDerivativeVector C ψ w)
have hbeta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) beta :=
IsCrossedDifferential.map_linear (zcFreeGroupFoxDerivativeVector_isCrossedDifferential C ψ) L
have hbasis : ∀ x : X, beta (FreeGroup.of x) = delta (FreeGroup.of x) := by
intro x
simp only [zcFreeCrossedDifferentialCoordinateLift, LinearMap.coe_mk, AddHom.coe_mk,
zcFreeGroupFoxDerivativeVector_of, Fintype.sum_single_smul, one_smul, beta, L]
have hbeta_eq :
beta =
freeCrossedDifferentialWithCoeff
(A := A) (zcCompletedGroupAlgebraScalar C ψ)
(fun x : X => delta (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := A) (zcCompletedGroupAlgebraScalar C ψ)
(fun x : X => delta (FreeGroup.of x)) beta hbeta hbasis
have hdelta_eq :
delta =
freeCrossedDifferentialWithCoeff
(A := A) (zcCompletedGroupAlgebraScalar C ψ)
(fun x : X => delta (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := A) (zcCompletedGroupAlgebraScalar C ψ)
(fun x : X => delta (FreeGroup.of x)) delta hdelta (by intro x; rfl)
simpa [beta, L] using congrFun (hbeta_eq.trans hdelta_eq.symm) wProof. 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. 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 zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates
(ψ : FreeGroup X →* H) (delta : FreeGroup X → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
zcFreeCrossedDifferentialCoordinateLift (H := H) C delta =
(zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta).comp
(zcFreeFoxCoordinatesLinearMap C ψ)The coordinate lift is obtained by composing the representing universal-module lift with the coordinate-to-module map.
Show proof
by
ext v
simp only [zcFreeCrossedDifferentialCoordinateLift, LinearMap.coe_mk, AddHom.coe_mk,
zcFreeFoxCoordinatesLinearMap, LinearMap.coe_comp, Function.comp_apply, map_sum, map_smul,
zcCompletedDifferentialModuleLift_universal]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. 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 zcCompletedDifferentialModuleLift_eq_coordinateLift_comp
(ψ : FreeGroup X →* H) (delta : FreeGroup X → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta =
(zcFreeCrossedDifferentialCoordinateLift (H := H) C delta).comp
(zcDifferentialToFreeFoxCoordinates C ψ)The representing universal-module lift factors through completed Fox coordinates.
Show proof
by
apply zcCompletedDifferentialModuleHom_ext C ψ
intro w
simp only [zcCompletedDifferentialModuleLift_universal, LinearMap.comp_apply,
zcDifferentialToFreeFoxCoordinates_universal,
zcFreeCrossedDifferentialCoordinateLift_derivativeVector C ψ delta hdelta 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\). 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. 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 continuous_zcCompletedDifferentialModuleLift_freeTopology_iff
{ψ : FreeGroup X →* H} {delta : FreeGroup X → A}
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
@Continuous (ZCCompletedDifferentialModule C ψ) A
(zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
(zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) ↔
Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)The completed differential-module criterion is equivalent to the corresponding finite-stage coordinate condition.
Show proof
by
constructor
· intro h
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleFreeTopology C ψ
have h' : Continuous (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) := h
have hcoord :=
continuous_zcFreeFoxCoordinatesLinearMap_freeTopology (X := X) (H := H) C ψ
have heq :=
zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates
(A := A) C ψ delta hdelta
simpa [heq, LinearMap.comp_apply] using h'.comp hcoord
· intro h
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleFreeTopology C ψ
have hcoord :=
continuous_zcDifferentialToFreeFoxCoordinates_freeTopology (X := X) (H := H) C ψ
have heq :=
zcCompletedDifferentialModuleLift_eq_coordinateLift_comp
(A := A) C ψ delta hdelta
simpa [heq, LinearMap.comp_apply] using h.comp hcoordProof. 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. Exactness is proved by identifying the image of the previous boundary map with the elements whose Fox coordinates vanish under the next boundary map, giving both inclusions at the finite stages. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□instance zcCompletedDifferentialModuleFreeTopologyInst :
TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleFreeTopology C ψThe free completed differential pre-module carries the finite-stage topology used before quotienting by crossed-differential relations.
def zcDifferentialToFreeFoxCoordinatesContinuousLinearMap :
ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := X) (H := H) where
toLinearMap := zcDifferentialToFreeFoxCoordinates C ψ
cont := continuous_zcDifferentialToFreeFoxCoordinates_freeTopology (X := X) (H := H) C ψThe completed coordinate map is bundled into a continuous linear map for the coordinate-induced topology.
theorem zcDifferentialToFreeFoxCoordinatesContinuousLinearMap_apply
(m : ZCCompletedDifferentialModule C ψ) :
zcDifferentialToFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ m =
zcDifferentialToFreeFoxCoordinates C ψ mEvaluation of the continuous completed coordinate map.
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.
□def zcFreeFoxCoordinatesContinuousLinearMap :
ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H]
ZCCompletedDifferentialModule C ψ where
toLinearMap := zcFreeFoxCoordinatesLinearMap C ψ
cont := continuous_zcFreeFoxCoordinatesLinearMap_freeTopology (X := X) (H := H) C ψThe coordinate-to-universal map as a continuous linear map for the coordinate-induced topology.
theorem zcFreeFoxCoordinatesContinuousLinearMap_apply
(v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ v =
zcFreeFoxCoordinatesLinearMap C ψ vEvaluation of the continuous coordinate-to-universal map.
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.
□def zcFreeCrossedDifferentialCoordinateContinuousLinearMap
(delta : FreeGroup X → A)
(hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H] A where
toLinearMap := zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
cont := hcontA finite coordinate lift is bundled as a continuous linear map once its continuity is known.
theorem zcFreeCrossedDifferentialCoordinateContinuousLinearMap_apply
(delta : FreeGroup X → A)
(hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
(v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcFreeCrossedDifferentialCoordinateContinuousLinearMap
(X := X) (H := H) (A := A) C delta hcont v =
∑ x : X, v x • delta (FreeGroup.of x)Evaluation of the continuous coordinate lift attached to generator values.
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.
□def zcCompletedDifferentialModuleLiftContinuousLinearMap
(delta : FreeGroup X → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcont : Continuous (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta)) :
ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
toLinearMap := zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta
cont := hcontThe representing universal lift is bundled as a continuous linear map once its continuity for the coordinate-induced topology is known.
theorem zcCompletedDifferentialModuleLiftContinuousLinearMap_apply
(delta : FreeGroup X → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcont : Continuous (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta))
(m : ZCCompletedDifferentialModule C ψ) :
zcCompletedDifferentialModuleLiftContinuousLinearMap
(X := X) (H := H) (A := A) C ψ delta hdelta hcont m =
zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta mEvaluation of the continuous representing universal lift.
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.
□def zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
(delta : FreeGroup X → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A :=
zcCompletedDifferentialModuleLiftContinuousLinearMap
(X := X) (H := H) (A := A) C ψ delta hdelta
((continuous_zcCompletedDifferentialModuleLift_freeTopology_iff
(X := X) (H := H) (A := A) (ψ := ψ) (delta := delta) hdelta).2 hcoord)Continuous representation theorem packaged as a continuous linear map: it is enough to prove continuity of the finite coordinate lift.
theorem zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate_apply
(delta : FreeGroup X → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
(m : ZCCompletedDifferentialModule C ψ) :
zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
(X := X) (H := H) (A := A) C ψ delta hdelta hcoord m =
zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta mEvaluation of the continuous universal lift obtained from a continuous finite coordinate lift.
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.
□