FoxDifferential.Completed.FreeProC.RelationSubmoduleApproximation
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
import
theorem boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))
(hbasis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J,
π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
(hstage_module_exact :
∀ j : J,
finiteFoxStageRelationBoundaryModuleExact
(X := X) (Nstage j) (nstage j))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hkernel_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Completed Fox density from finite-stage relation-submodule exactness.
Show proof
by
refine
freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage ?_
hNstage_kernel hkernel_word_projection
intro j
exact finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
(X := X) (Nstage j) (nstage j) (hstage_module_exact j)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\). 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. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relSubmodule_exact
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))
(hbasis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J,
π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
(hstage_module_exact :
∀ j : J,
finiteFoxStageRelationBoundaryModuleExact
(X := X) (Nstage j) (nstage j))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hkernel_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (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 finite relation-submodule input places completed boundary cycles in the closed generated Fox graph target.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage
hstage_module_exact hNstage_kernel hkernel_word_projection)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\). 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. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))
(hbasis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J,
π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
(hstage_reduce :
∀ j : J,
finiteFoxStageSourceBoundaryRelationIdealReduction
(X := X) (Nstage j) (nstage j))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hkernel_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Completed Fox density from the source-boundary relation-ideal reduction at every finite stage. This is the next attack route below relation-submodule exactness: instead of assuming finite module exactness directly, it suffices to prove that source-coordinate lifts whose source boundary lies in the explicit relation augmentation ideal project to relation-boundary vectors.
Show proof
by
refine
boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage ?_
hNstage_kernel hkernel_word_projection
intro j
exact finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
(X := X) (Nstage j) (nstage j) (hstage_reduce j)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. 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. For the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))
(hbasis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J,
π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
(hstage_reduce :
∀ j : J,
finiteFoxStageSourceBoundaryRelationIdealReduction
(X := X) (Nstage j) (nstage j))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hkernel_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (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 source-boundary relation-ideal route also places completed boundary cycles inside the closed-generated Fox graph target.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage
hstage_reduce hNstage_kernel hkernel_word_projection)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\). 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. 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_closure_kernelCycleSet_of_finiteStage_relDeriv
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))
(hbasis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J,
π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hkernel_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Show proof
by
refine
boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage ?_
hNstage_kernel hkernel_word_projection
intro j
exact finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives
(X := X) (Nstage j) (nstage j)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. 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_closedGenTarget_of_finiteStage_relDeriv
[Fintype X] (φ : X → H)
{J : Type v}
(Nstage : J → Subgroup (FreeGroup X))
[∀ j, (Nstage j).Normal]
(nstage : J → ℕ)
(π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j))
(hbasis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J,
π j y ∈ finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
(hNstage_kernel :
∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
(hkernel_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (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))Completed boundary cycles lie in the closed-generated Fox graph target using the finite-stage relation-ideal derivative theorem.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage
hNstage_kernel hkernel_word_projection)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\). 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. 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.
□