FoxDifferential.Completed.FreeProC.StageProjection
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
def freeProCZCCompletedFoxSemidirectStageMap
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v) :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) N n where
toFun y :=
{ left := stageLeft y.left
right := stageRight y.right }
map_one' := by
apply FiniteFoxStageSemidirect.ext
· change stageLeft 0 = 0
exact map_zero stageLeft
· exact map_one stageRight
map_mul' a b := by
apply FiniteFoxStageSemidirect.ext
· change
stageLeft (a.left + zcGroupLike ProC.finiteQuotientClass H a.right • b.left) =
stageLeft a.left +
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight a.right)) •
stageLeft b.left
rw [map_add, hscalar]
· change stageRight (a.right * b.right) = stageRight a.right * stageRight b.right
exact map_mul stageRight a.right b.rightA semidirect projection from the completed Fox semidirect product to a finite Fox stage, constructed from a left coordinate map and a right target quotient map. The only compatibility required is that the left coordinate map respects the scalar action used in semidirect multiplication. This is the abstract form of the finite quotient map \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H \to ((\mathbb{Z}/n\mathbb{Z})[F/N])^X \rtimes F/N\).
theorem freeProCZCCompletedFoxSemidirectStageMap_left
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
(freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y).left =
stageLeft y.leftShow 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 freeProCZCCompletedFoxSemidirectStageMap_right
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
(freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y).right =
stageRight y.rightThe right coordinate of the 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 freeProCZCCompletedFoxSemidirectStageMap_mem_ker_iff
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
{y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H} :
y ∈ (freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar).ker ↔
stageLeft y.left = 0 ∧ stageRight y.right = 1Membership in the kernel of the completed Fox semidirect stage map is equivalent to vanishing of the corresponding finite-stage coordinate.
Show proof
by
constructor
· intro hy
change
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y = 1 at hy
have hleft := congrArg (fun z : FiniteFoxStageSemidirect (X := X) N n => z.left) hy
have hright := congrArg (fun z : FiniteFoxStageSemidirect (X := X) N n => z.right) hy
exact ⟨by simpa using hleft, by simpa using hright⟩
· rintro ⟨hleft, hright⟩
change
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y = 1
apply FiniteFoxStageSemidirect.ext
· simpa using hleft
· simpa using hrightProof. 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 freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet
[Fintype X]
(φ : X → H)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(stageBoundary :
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) N n)
(hboundary :
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) N n (stageLeft v) =
stageBoundary
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
{y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
(hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ) :
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y ∈
finiteFoxStageSemidirectBoundaryCycleSet (X := X) N nA completed boundary-cycle point projects to a finite boundary-cycle point once the left coordinate projection commutes with the source-shaped Fox boundary.
Show proof
by
rcases hy with ⟨hyright, hyboundary⟩
constructor
· change stageRight y.right = 1
rw [hyright]
exact map_one stageRight
· rw [mem_finiteFoxStageBoundaryCycleSubmodule]
calc
finiteFoxStageFoxBoundary (X := X) N n
((freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y).left)
= finiteFoxStageFoxBoundary (X := X) N n (stageLeft y.left) := rfl
_ = stageBoundary
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) y.left) :=
hboundary y.left
_ = 0 := by
rw [hyboundary]
exact map_zero stageBoundaryProof. 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 freeProCZCCompletedFoxSemidirectStageMap_kernelWordPoint
(φ : X → H)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(hderivative :
∀ w : FreeGroup X,
stageLeft
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) N n w)
(w : FreeGroup X) :
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar
(freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) N n wThe stage map sends the completed kernel-word point \((D w, 1)\) to the corresponding finite kernel-word point, provided the left coordinate projection commutes with Fox derivatives.
Show proof
by
apply FiniteFoxStageSemidirect.ext
· change
stageLeft
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) N n w
exact hderivative w
· simp only [freeProCZCCompletedFoxSemidirectKernelWordPoint, freeProCZCCompletedFoxSemidirectStageMap_right,
map_one, finiteFoxStageSemidirectKernelWordPoint]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. 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 freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint
(φ : X → H)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(hderivative :
∀ w : FreeGroup X,
stageLeft
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) N n w)
(w : FreeGroup X) :
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar
(freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w) =
({ left := finiteFoxStageDerivativeVector (X := X) N n w,
right := stageRight (FreeGroup.lift φ w) } :
FiniteFoxStageSemidirect (X := X) N n)The stage map sends a completed graph-word point \((D w,\varphi(w))\) to the corresponding finite stage graph point.
Show proof
by
apply FiniteFoxStageSemidirect.ext
· exact hderivative w
· 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 freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint_of_stage_kernel
(φ : X → H)
(stageLeft :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) N n)
(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 n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
stageLeft v)
(hderivative :
∀ w : FreeGroup X,
stageLeft
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) N n w)
(hright_word :
∀ w : FreeGroup X, stageRight (FreeGroup.lift φ w) = QuotientGroup.mk' N w)
(w : FreeGroup X) (hw : w ∈ N) :
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar
(freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) N n wShow proof
by
rw [freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint
(ProC := ProC) (X := X) (H := H) N n φ stageLeft stageRight hscalar hderivative w]
apply FiniteFoxStageSemidirect.ext
· rfl
· change stageRight (FreeGroup.lift φ w) = 1
rw [hright_word w]
exact (QuotientGroup.eq_one_iff (N := N) w).2 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. 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. 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 freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hquotient_basis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Completed Fox density from a family of concrete completed-to-finite semidirect stage maps. The finite exactness input is the relation-ideal derivative theorem already proved at every finite stage. The remaining data are now exactly the two projection formulas expected from the completed Fox construction: boundary compatibility and derivative compatibility.
Show proof
by
let π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j) :=
fun j =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)
refine
freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv
(ProC := ProC) φ Nstage nstage π ?_ ?_ hNstage_kernel ?_
· exact hquotient_basis
· intro y hy j
exact
freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
φ (stageLeft j) (stageRight j) (hscalar j) (stageBoundary j)
(hboundary j) hy
· intro j w hw
exact
freeProCZCCompletedFoxSemidirectStageMap_kernelWordPoint
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
φ (stageLeft j) (stageRight j) (hscalar j) (hderivative j) 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. 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. 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.
□theorem freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hquotient_basis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hright_word :
∀ j : J, ∀ w : FreeGroup X,
stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ)Completed graph-word density from concrete completed-to-finite semidirect stage maps. Unlike the kernel-word route, this theorem does not assume that \(w \in N_{\mathrm{stage},j}\) implies \(\mathrm{FreeGroup.lift}(\varphi)(w)=1\). Finite-stage exactness supplies \(w \in N_{\mathrm{stage},j}\), and the completed approximating point is the graph point \((D w, \varphi(w))\).
Show proof
by
let π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j) :=
fun j =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)
refine
freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_exact
(ProC := ProC) φ Nstage nstage π ?_ ?_ ?_ ?_
· exact hquotient_basis
· intro y hy j
exact
freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
φ (stageLeft j) (stageRight j) (hscalar j) (stageBoundary j)
(hboundary j) hy
· intro j
exact finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives
(X := X) (Nstage j) (nstage j)
· intro j w hw
exact
freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint_of_stage_kernel
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
φ (stageLeft j) (stageRight j) (hscalar j) (hderivative j)
(hright_word j) w 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. 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. 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.
□theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_graphRelDeriv
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hquotient_basis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hright_word :
∀ j : J, ∀ w : FreeGroup X,
stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Concrete stage-map graph-word density, phrased as closed-generated-target membership.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density
(ProC := ProC) φ
(freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv
(ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hquotient_basis
stageBoundary hboundary hright_word 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.
□theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_relDeriv
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hquotient_basis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))The same concrete stage-map route, with the conclusion phrased as membership in the closed-generated Fox graph target.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv
(ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hquotient_basis
stageBoundary hboundary hNstage_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.
□theorem boundaryCycles_subset_kernelClosure_of_stageMaps
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hidentity_basis :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Stage-map density is formulated using identity-neighborhood kernels rather than left-coset kernels. This is the topological form produced by separation through finite quotients in profinite groups. The conversion to the left-coset closure basis is performed internally.
Show proof
by
refine
freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv
(ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar ?_
stageBoundary hboundary hNstage_kernel hderivative
exact HasIdentityQuotientKernelNeighbourhoodBasis.to_left
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(π := fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j))
hidentity_basisProof. 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. 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 boundaryCycles_subset_graphWordClosure_of_stageMaps
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hidentity_basis :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hright_word :
∀ j : J, ∀ w : FreeGroup X,
stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ)Graph-word density using identity-neighborhood kernels rather than left-coset kernels.
Show proof
by
refine
freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv
(ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar ?_
stageBoundary hboundary hright_word hderivative
exact HasIdentityQuotientKernelNeighbourhoodBasis.to_left
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(π := fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j))
hidentity_basisProof. 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_stageGraph
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hidentity_basis :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hright_word :
∀ j : J, ∀ w : FreeGroup X,
stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) 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 identity-kernel graph-word stage-map theorem.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density
(ProC := ProC) φ
(boundaryCycles_subset_graphWordClosure_of_stageMaps
(ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hidentity_basis
stageBoundary hboundary hright_word 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. 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 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_identityKernel_relDeriv
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(stageLeft : ∀ j : J,
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
(stageRight : ∀ j : J,
H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
(hscalar :
∀ j : J, ∀ (h : H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
(MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
(finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
stageLeft j v)
(hidentity_basis :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(fun j : J =>
freeProCZCCompletedFoxSemidirectStageMap
(ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
(stageLeft j) (stageRight j) (hscalar j)))
(stageBoundary : ∀ j : J,
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))
(hboundary :
∀ j : J,
∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =
stageBoundary j
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hderivative :
∀ j : J, ∀ w : FreeGroup X,
stageLeft j
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w) =
finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) 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 identity-kernel stage-map density theorem.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(boundaryCycles_subset_kernelClosure_of_stageMaps
(ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hidentity_basis
stageBoundary hboundary hNstage_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. 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.
□