import
theorem subset_closure_of_quotientKernel_stage_exact
{J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
(π : ∀ j : J, Y →* Q j)
(hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
(Sstage Tstage : ∀ j : J, Set (Q j))
(hTstage : ∀ y : Y, y ∈ T → ∀ j : J, π j y ∈ Tstage j)
(hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)
(hlift_stage : ∀ j : J, ∀ q : Q j, q ∈ Sstage j →
∃ s : Y, s ∈ S ∧ π j s = q) :
T ⊆ closure SQuotient-kernel density from exact finite-stage images. For each quotient stage \(j\), let \(T_{\mathrm{stage}}(j)\) be the image condition satisfied by points of \(T\), and let \(S_{\mathrm{stage}}(j)\) be the finite-stage image of algebraic approximants from \(S\). If every \(T_{\mathrm{stage}}\) point is in \(S_{\mathrm{stage}}\), and every \(S_{\mathrm{stage}}\) point lifts to an actual point of \(S\), then \(T\) is contained in the closure of \(S\).
Show proof
by
refine subset_closure_of_quotientKernel_approximation π hbasis ?_
intro y hy j
exact hlift_stage j (π j y) (hstage_exact j (hTstage y hy 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_closure_kernelCycleSet_of_stage_exact
[Fintype X] (φ : X → H)
{J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
(π : ∀ j : J,
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →* Q j)
(hbasis :
HasLeftQuotientKernelNeighbourhoodBasis
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
(Sstage Tstage : ∀ j : J, Set (Q j))
(hboundary_stage :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J, π j y ∈ Tstage j)
(hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)
(hlift_stage :
∀ j : J, ∀ q : Q j, q ∈ Sstage j →
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) = q) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Completed Fox density from exactness of arbitrary quotient-stage images. This is the general completed semidirect bridge: choose quotient maps out of the completed semidirect product, prove that boundary cycles land in the chosen finite-stage \(T_{\mathrm{stage}}\), prove finite-stage exactness \(T_{\mathrm{stage}}\) \(\subseteq\) \(S_{\mathrm{stage}}\), and lift every \(S_{\mathrm{stage}}\) point to an actual kernel word.
Show proof
by
refine subset_closure_of_quotientKernel_stage_exact
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(S := freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)
(T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)
π hbasis Sstage Tstage hboundary_stage hstage_exact ?_
intro j q hq
rcases hlift_stage j q hq with ⟨w, hw, hπw⟩
refine ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w, ?_, hπw⟩
exact freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
(ProC := ProC) φ 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\). 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_closure_kernelCycleSet_of_finiteStage_semi_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_exact :
∀ j : J,
finiteFoxStageBoundaryCyclesCoveredBySourceKernel
(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 semidirect Fox exactness at every quotient stage. Here the finite-stage \(T_{\mathrm{stage}}\) is the set of finite semidirect boundary cycles and the finite-stage \(S_{\mathrm{stage}}\) is the set of actual kernel-word derivative points. The hypotheses that remain are the actual comparison data between completed stages and finite Fox stages.
Show proof
by
refine
freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stage_exact
(ProC := ProC) φ π hbasis
(fun j => finiteFoxStageSemidirectKernelWordDerivativeSet
(X := X) (Nstage j) (nstage j))
(fun j => finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
hboundary_stage ?_ ?_
· intro j
exact
(finiteFoxStageSemidirectBoundaryCyclesCoveredByKernelWords_iff
(X := X) (Nstage j) (nstage j)).2 (hstage_exact j)
· intro j q hq
rcases hq with ⟨w, hwN, hpoint⟩
refine ⟨w, hNstage_kernel j hwN, ?_⟩
calc
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w)
= finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w :=
hkernel_word_projection j w hwN
_ = q := hpointProof. 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_closure_graphWordSet_of_finiteStage_semi_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_exact :
∀ j : J,
finiteFoxStageBoundaryCyclesCoveredBySourceKernel
(X := X) (Nstage j) (nstage j))
(hgraph_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ)Completed Fox graph-word density from finite semidirect Fox exactness at every quotient stage. This is the finite-quotient form that does not assume that words in the finite relation subgroup \(N_{\mathrm{stage},j}\) to be actual kernel words for \(\varphi\). A word \(w \in N_{\mathrm{stage},j}\) only has to project to the trivial right coordinate at the \(j\)-th finite stage; the completed approximant remains the genuine graph point \((D w, \varphi(w))\).
Show proof
by
refine subset_closure_of_quotientKernel_stage_exact
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(S := freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ)
(T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)
π hbasis
(fun j => finiteFoxStageSemidirectKernelWordDerivativeSet
(X := X) (Nstage j) (nstage j))
(fun j => finiteFoxStageSemidirectBoundaryCycleSet
(X := X) (Nstage j) (nstage j))
hboundary_stage ?_ ?_
· intro j
exact
(finiteFoxStageSemidirectBoundaryCyclesCoveredByKernelWords_iff
(X := X) (Nstage j) (nstage j)).2 (hstage_exact j)
· intro j q hq
rcases hq with ⟨w, hwN, hpoint⟩
refine ⟨freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w, ?_, ?_⟩
· exact ⟨w, rfl⟩
· calc
π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w)
= finiteFoxStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w :=
hgraph_word_projection j w hwN
_ = q := hpointProof. 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_finiteStage_graphWord_semi_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_exact :
∀ j : J,
finiteFoxStageBoundaryCyclesCoveredBySourceKernel
(X := X) (Nstage j) (nstage j))
(hgraph_word_projection :
∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (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))Finite-stage semidirect exactness places every completed boundary cycle in the closed generated Fox graph target without assuming that finite relation words are actual kernel words.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density
(ProC := ProC) φ
(freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_exact
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage hstage_exact
hgraph_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 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_semi_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_exact :
∀ j : J,
finiteFoxStageBoundaryCyclesCoveredBySourceKernel
(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 finite-stage semidirect exactness route also places every completed boundary cycle in the closed generated Fox graph target.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact
(ProC := ProC) φ Nstage nstage π hbasis hboundary_stage hstage_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\). 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.
□