FoxDifferential.Completed.Continuous.Universal.System
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
def zcCompletedDifferentialModuleStageSystem :
InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
X := fun i => ZCCompletedDifferentialModuleStage C ψ i
topologicalSpace := fun _ => ⊥
map := fun {i j} hij => zcCompletedDifferentialModuleStageTransition C ψ hij
continuous_map := by
intro i j hij
letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := ⊥
letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ j) := ⊥
letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ j) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro i
funext x
exact congrFun
(congrArg DFunLike.coe
(zcCompletedDifferentialModuleStageTransition_id C ψ i)) x
map_comp := by
intro i j k hij hjk
funext x
exact congrFun
(congrArg DFunLike.coe
(zcCompletedDifferentialModuleStageTransition_comp C ψ hij hjk)) xThe inverse system of finite source, target, and coefficient stages of \(A_{\psi}(C)\).
instance instAddCommGroupZCCompletedDifferentialModuleStageSystemStage
(i : ZCCompletedDifferentialModuleIndex C ψ) :
AddCommGroup ((zcCompletedDifferentialModuleStageSystem C ψ).X i) := by
dsimp [zcCompletedDifferentialModuleStageSystem]
infer_instanceAddition in the finite-stage completed differential-module system is defined coordinatewise.
instance instIsAddGroupSystemZCCompletedDifferentialModuleStageSystem :
IsAddGroupSystem (zcCompletedDifferentialModuleStageSystem C ψ) where
map_zero := by
intro i j hij
exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_zero
map_add := by
intro i j hij x y
exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_add x y
map_neg := by
intro i j hij x
exact map_neg (zcCompletedDifferentialModuleStageTransition C ψ hij) xThe inverse system of finite-stage group algebras has addition defined coordinatewise on compatible families.
theorem zcCompletedDifferentialModuleStageSystem_map_apply
{i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
(x : ZCCompletedDifferentialModuleStage C ψ j) :
(zcCompletedDifferentialModuleStageSystem C ψ).map hij x =
zcCompletedDifferentialModuleStageTransition C ψ hij xThe system map on completed differential modules is evaluated coordinatewise at each finite coefficient stage.
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 zcCompletedDifferentialModuleStageSystem_projection_compatible
(x : (zcCompletedDifferentialModuleStageSystem C ψ).inverseLimit)
(i j : ZCCompletedDifferentialModuleIndex C ψ) (hij : i ≤ j) :
zcCompletedDifferentialModuleStageTransition C ψ hij
((zcCompletedDifferentialModuleStageSystem C ψ).projection j x) =
(zcCompletedDifferentialModuleStageSystem C ψ).projection i xInverse-limit projections of the finite \(A_{\psi}(C)\) stage system are compatible with transition maps.
Show proof
(zcCompletedDifferentialModuleStageSystem C ψ).projection_compatible x i j hijProof. 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. 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 zcCompletedDifferentialPreModuleStageSystem :
InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
X := fun i =>
CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)
topologicalSpace := fun _ => ⊥
map := fun {i j} hij => zcCompletedDifferentialModulePreStageTransition C ψ hij
continuous_map := by
intro i j hij
letI : TopologicalSpace
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) := ⊥
letI : TopologicalSpace
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ j)
(zcCompletedDifferentialModuleStageSource C ψ j)) := ⊥
letI : DiscreteTopology
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ j)
(zcCompletedDifferentialModuleStageSource C ψ j)) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro i
funext x
exact congrFun
(congrArg DFunLike.coe
(zcCompletedDifferentialModulePreStageTransition_id C ψ i)) x
map_comp := by
intro i j k hij hjk
funext x
exact congrFun
(congrArg DFunLike.coe
(zcCompletedDifferentialModulePreStageTransition_comp C ψ hij hjk)) xThe inverse system of finite pre-modules before quotienting by crossed-differential relations.
abbrev ZCCompletedDifferentialPreModuleStageFamily : Type u :=
(zcCompletedDifferentialPreModuleStageSystem C ψ).inverseLimitCompatible inverse-limit families of finite pre-stage elements.
theorem zcCompletedDifferentialPreModuleStageSystem_map_apply
{i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
(x : CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ j)
(zcCompletedDifferentialModuleStageSource C ψ j)) :
(zcCompletedDifferentialPreModuleStageSystem C ψ).map hij x =
zcCompletedDifferentialModulePreStageTransition C ψ hij xThe system map on completed differential modules is evaluated coordinatewise at each finite coefficient stage.
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 zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap :
(zcCompletedDifferentialPreModuleStageSystem C ψ).CompatibleMaps
(fun i : ZCCompletedDifferentialModuleIndex C ψ =>
zcCompletedDifferentialModulePreStageMap C ψ i)The explicit finite pre-stage reductions of a completed pre-module element are compatible with finite transitions.
Show proof
by
intro i j hij
funext x
exact zcCompletedDifferentialModulePreStageTransition_preStageMap C ψ hij 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\). 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.
□def zcCompletedDifferentialPreModuleStageFamilyMap :
CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →
ZCCompletedDifferentialPreModuleStageFamily C ψ :=
(zcCompletedDifferentialPreModuleStageSystem C ψ).inverseLimitLift
(fun i : ZCCompletedDifferentialModuleIndex C ψ =>
zcCompletedDifferentialModulePreStageMap C ψ i)
(zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap C ψ)The finite-stage family map sends a completed pre-module element to its compatible family of finite source, target, and coefficient stages.
theorem zcCompletedDifferentialPreModuleStageFamilyMap_projection
(i : ZCCompletedDifferentialModuleIndex C ψ)
(x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
(zcCompletedDifferentialPreModuleStageSystem C ψ).projection i
(zcCompletedDifferentialPreModuleStageFamilyMap C ψ x) =
zcCompletedDifferentialModulePreStageMap C ψ i xProjecting the finite-stage pre-module family map at a stage recovers the explicit pre-stage map at that stage.
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. 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.
□