FoxDifferential.Completed.FreeProC.PrimePowerStageProjection
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
def freeProCZCCompletedFoxSemidirectPrimePowerStageMap
(a : ℕ)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
(stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
(hscalar :
∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v) :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) N (ℓ ^ a) :=
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N (ℓ ^ a) stageLeft stageRight hscalarA completed Fox semidirect projection to the \(\ell^a\) finite stage.
theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_left
(a : ℕ)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
(stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
(hscalar :
∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
(freeProCZCCompletedFoxSemidirectPrimePowerStageMap
(ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y).left =
stageLeft y.leftThe left component of the prime-power finite-stage semidirect map is the prescribed coordinate map applied to the source component.
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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_right
(a : ℕ)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
(stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
(hscalar :
∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
(freeProCZCCompletedFoxSemidirectPrimePowerStageMap
(ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y).right =
stageRight y.rightThe right coordinate of the prime-power completed Fox semidirect stage map is the selected target quotient 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. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_mem_finiteBoundaryCycleSet
[Fintype X]
(φ : X → H) (a : ℕ)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
(stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
(hscalar :
∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(stageBoundary :
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) N (ℓ ^ a))
(hboundary :
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft v) =
stageBoundary
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
{y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
(hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ) :
freeProCZCCompletedFoxSemidirectPrimePowerStageMap
(ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y ∈
finiteFoxStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ a)Boundary-cycle preservation for a prime-power completed-to-finite stage map.
Show proof
by
exact
freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet
(ProC := ProC) (X := X) (H := H) N (ℓ ^ a) φ
stageLeft stageRight hscalar stageBoundary hboundary hyProof. 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. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_kernelWordPoint
(φ : X → H) (a : ℕ)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
(stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
(hscalar :
∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(hderivative :
∀ w : FreeGroup X,
stageLeft
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) N (ℓ ^ a) w)
(w : FreeGroup X) :
freeProCZCCompletedFoxSemidirectPrimePowerStageMap
(ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar
(freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) N (ℓ ^ a) wKernel-word points project to kernel-word points at prime-power finite stages.
Show proof
by
exact
freeProCZCCompletedFoxSemidirectStageMap_kernelWordPoint
(ProC := ProC) (X := X) (H := H) N (ℓ ^ a) φ
stageLeft stageRight hscalar hderivative 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. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
(π : ∀ a : ℕ,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
(hπ : ∀ {a b : ℕ} (hab : a ≤ b),
(finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
π a) :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N where
toFun y :=
⟨fun a => π a y, by
intro a b hab
exact congrArg (fun f => f y) (hπ hab)⟩
map_one' := by
apply Subtype.ext
funext a
exact map_one (π a)
map_mul' y z := by
apply Subtype.ext
funext a
exact map_mul (π a) y zAssemble compatible prime-power stage maps into a map to the inverse limit of finite semidirect stages.
theorem freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_projection
(π : ∀ a : ℕ,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
(hπ : ∀ {a b : ℕ} (hab : a ≤ b),
(finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
π a)
(a : ℕ) (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
finiteFoxStagePrimePowerSemidirectLimitProjection (ℓ := ℓ) (X := X) N a
(freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
(ProC := ProC) (X := X) (H := H) ℓ N π hπ y) =
π a yProjection after the free pro-\(C\) \(\mathbb{Z}_C\)-completed Fox semidirect prime-power limit map is computed by the finite-stage 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. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_mem_boundaryCycleSet
[Fintype X] (φ : X → H)
(π : ∀ a : ℕ,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
(hπ : ∀ {a b : ℕ} (hab : a ≤ b),
(finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
π a)
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ a : ℕ, π a y ∈ finiteFoxStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ a))
{y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
(hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ) :
freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
(ProC := ProC) (X := X) (H := H) ℓ N π hπ y ∈
finiteFoxStagePrimePowerSemidirectLimitBoundaryCycleSet (ℓ := ℓ) (X := X) NA completed boundary-cycle point maps to a stagewise boundary-cycle point in the prime-power inverse limit.
Show proof
by
intro a
simpa using hboundary_stage y hy aProof. 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\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_kernelWordPoint
(φ : X → H)
(π : ∀ a : ℕ,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
(hπ : ∀ {a b : ℕ} (hab : a ≤ b),
(finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
π a)
(hkernel_word_projection :
∀ a : ℕ, ∀ w : FreeGroup X,
π a (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) N (ℓ ^ a) w)
(w : FreeGroup X) :
freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
(ProC := ProC) (X := X) (H := H) ℓ N π hπ
(freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStagePrimePowerSemidirectKernelWordPointLimit (ℓ := ℓ) (X := X) N wKernel-word points commute with the prime-power inverse-limit map.
Show proof
by
apply Subtype.ext
funext a
exact hkernel_word_projection a 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\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem boundaryCycles_subset_kernelClosure_of_ppStageMaps
[Fintype X] (φ : X → H)
(stageLeft : ∀ a : ℕ,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
(stageRight : ∀ _a : ℕ,
H →* finiteFoxStageTargetQuotient (X := X) N)
(hscalar :
∀ a : ℕ, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft a (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
(finiteFoxStageTargetQuotient (X := X) N) (stageRight a h)) •
stageLeft a v)
(hidentity_basis :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun a : ℕ =>
freeProCZCCompletedFoxSemidirectPrimePowerStageMap
(ProC := ProC) (X := X) (H := H) ℓ N a
(stageLeft a) (stageRight a) (hscalar a)))
(stageBoundary : ∀ a : ℕ,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) N (ℓ ^ a))
(hboundary :
∀ a : ℕ,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft a v) =
stageBoundary a
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hN_kernel : ∀ {w : FreeGroup X}, w ∈ N → FreeGroup.lift φ w = 1)
(hderivative :
∀ a : ℕ, ∀ w : FreeGroup X,
stageLeft a
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) N (ℓ ^ a) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Completed Fox density from prime-power stage maps and the finite relation-ideal derivative theorem.
Show proof
by
refine
boundaryCycles_subset_kernelClosure_of_stageMaps
(ProC := ProC) φ (fun _ : ℕ => N) (fun a : ℕ => ℓ ^ a)
stageLeft stageRight hscalar ?_ stageBoundary hboundary ?_ hderivative
· simpa [freeProCZCCompletedFoxSemidirectPrimePowerStageMap] using hidentity_basis
· intro _ w hw
exact hN_kernel hwProof. 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. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem boundaryCycles_subset_closedGenTarget_of_ppStageMaps
[Fintype X] (φ : X → H)
(stageLeft : ∀ a : ℕ,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
(stageRight : ∀ _a : ℕ,
H →* finiteFoxStageTargetQuotient (X := X) N)
(hscalar :
∀ a : ℕ, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft a (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
(finiteFoxStageTargetQuotient (X := X) N) (stageRight a h)) •
stageLeft a v)
(hidentity_basis :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun a : ℕ =>
freeProCZCCompletedFoxSemidirectPrimePowerStageMap
(ProC := ProC) (X := X) (H := H) ℓ N a
(stageLeft a) (stageRight a) (hscalar a)))
(stageBoundary : ∀ a : ℕ,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) N (ℓ ^ a))
(hboundary :
∀ a : ℕ,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft a v) =
stageBoundary a
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hN_kernel : ∀ {w : FreeGroup X}, w ∈ N → FreeGroup.lift φ w = 1)
(hderivative :
∀ a : ℕ, ∀ w : FreeGroup X,
stageLeft a
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) N (ℓ ^ a) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Closed-generated-target version of the prime-power stage-map density theorem.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(boundaryCycles_subset_kernelClosure_of_ppStageMaps
(ProC := ProC) (X := X) (H := H) ℓ N φ
stageLeft stageRight hscalar hidentity_basis stageBoundary hboundary hN_kernel
hderivative)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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□