FoxDifferential.Completed.FreeProC.Density
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem subset_closure_of_open_neighbourhood_approximation
(happrox :
∀ y : Y, y ∈ T → ∀ U : Set Y, IsOpen U → y ∈ U →
∃ s : Y, s ∈ S ∧ s ∈ U) :
T ⊆ closure SA direct neighborhood approximation criterion for set-theoretic closure. This is the form used when a finite-stage argument has already produced an algebraic point of S inside every open neighborhood of a boundary point.
Show proof
by
intro y hy
rw [mem_closure_iff]
intro U hU hyU
rcases happrox y hy U hU hyU with ⟨s, hsS, hsU⟩
exact ⟨s, hsU, hsS⟩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\). 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 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.
□def HasLeftOpenSubgroupNeighbourhoodBasis (Y : Type u) [Group Y] [TopologicalSpace Y] : Prop :=
∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
∃ V : Subgroup Y, IsOpen ((V : Subgroup Y) : Set Y) ∧
∀ z : Y, z ∈ V → y * z ∈ ULeft open subgroup neighborhood basis, expressed as a proposition rather than a structure. For every neighborhood \(U\) of \(y\), one can find an open subgroup \(V\) such that the left coset \(yV\) is contained in \(U\). This is the topological input used to pass from finite or open-subgroup approximations to ordinary closure.
def HasLeftOpenNormalSubgroupNeighbourhoodBasis
(Y : Type u) [Group Y] [TopologicalSpace Y] : Prop :=
∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
∃ V : Subgroup Y, V.Normal ∧ IsOpen ((V : Subgroup Y) : Set Y) ∧
∀ z : Y, z ∈ V → y * z ∈ UThis is the normal-subgroup version of the left open-subgroup neighborhood basis: in a profinite group, every identity neighborhood can be refined by an open normal subgroup.
theorem HasLeftOpenNormalSubgroupNeighbourhoodBasis.to_subgroup_basis
(hbasis : HasLeftOpenNormalSubgroupNeighbourhoodBasis Y) :
HasLeftOpenSubgroupNeighbourhoodBasis YThe normal-subgroup basis implies the subgroup basis.
Show proof
by
intro y U hU hyU
rcases hbasis y U hU hyU with ⟨V, _hVnormal, hVopen, hVcoset⟩
exact ⟨V, hVopen, hVcoset⟩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\). 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. 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 subset_closure_of_openSubgroup_approximation
(hbasis : HasLeftOpenSubgroupNeighbourhoodBasis Y)
(happrox :
∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
IsOpen ((V : Subgroup Y) : Set Y) →
∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
T ⊆ closure SClosure criterion using open-subgroup approximations. It is enough to approximate each y \(\in\) T modulo every open subgroup V, in the sense that for some s \(\in\) S the correction \(y{}^{-1} * s\) lies in V.
Show proof
by
refine subset_closure_of_open_neighbourhood_approximation ?_
intro y hy U hU hyU
rcases hbasis y U hU hyU with ⟨V, hVopen, hVcoset⟩
rcases happrox y hy V hVopen with ⟨s, hsS, hsV⟩
refine ⟨s, hsS, ?_⟩
have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
simpa [mul_assoc] using hcosetProof. 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\). 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. 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 subset_closure_of_openNormalSubgroup_approximation
(hbasis : HasLeftOpenNormalSubgroupNeighbourhoodBasis Y)
(happrox :
∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
V.Normal → IsOpen ((V : Subgroup Y) : Set Y) →
∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
T ⊆ closure SThe completed Fox graph or boundary-cycle set lies in the required closed generated submodule by finite-stage separation.
Show proof
by
refine subset_closure_of_open_neighbourhood_approximation ?_
intro y hy U hU hyU
rcases hbasis y U hU hyU with ⟨V, hVnormal, hVopen, hVcoset⟩
rcases happrox y hy V hVnormal hVopen with ⟨s, hsS, hsV⟩
refine ⟨s, hsS, ?_⟩
have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
simpa [mul_assoc] using hcosetProof. 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\). 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 finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem mem_closure_of_openSubgroup_approximation
(hbasis : HasLeftOpenSubgroupNeighbourhoodBasis Y)
{y : Y} (_hy : y ∈ T)
(happrox :
∀ V : Subgroup Y, IsOpen ((V : Subgroup Y) : Set Y) →
∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
y ∈ closure SCoset approximation gives a pointwise closure statement.
Show proof
by
rw [mem_closure_iff]
intro U hU hyU
rcases hbasis y U hU hyU with ⟨V, hVopen, hVcoset⟩
rcases happrox V hVopen with ⟨s, hsS, hsV⟩
refine ⟨s, ?_, hsS⟩
have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
simpa [mul_assoc] using hcosetProof. 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. 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 subset_closure_of_quotientKernel_approximation
{J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
(π : ∀ j : J, Y →* Q j)
(hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
(happrox :
∀ y : Y, y ∈ T → ∀ j : J,
∃ s : Y, s ∈ S ∧ π j s = π j y) :
T ⊆ closure SIf quotient kernels form a left neighborhood basis, then equality at every quotient stage gives closure. This is the abstract topology step for the remaining Crowell density theorem: finite quotient exactness supplies \(s\in S\) with \(\pi_j s = \pi_j y\); the quotient-kernel basis turns this into ordinary topological approximation.
Show proof
by
refine subset_closure_of_open_neighbourhood_approximation ?_
intro y hy U hU hyU
rcases hbasis y U hU hyU with ⟨j, hj⟩
rcases happrox y hy j with ⟨s, hsS, hπ⟩
have hker : y⁻¹ * s ∈ (π j).ker := by
change π j (y⁻¹ * s) = 1
rw [map_mul, map_inv, hπ]
simp only [inv_mul_cancel]
refine ⟨s, hsS, ?_⟩
have hsU : y * (y⁻¹ * s) ∈ U := hj (y⁻¹ * s) hker
simpa [mul_assoc] using hsUProof. 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.
□def freeProCZCCompletedFoxSemidirectKernelWordPoint (φ : X → H) (w : FreeGroup X) :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
{ left :=
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
right := (1 : H) }The semidirect point \((D w, 1)\) attached to an abstract free-group kernel-word candidate. The word may or may not actually lie in the kernel; kernel membership is recorded separately by the corresponding kernel-cycle-set lemma.
theorem freeProCZCCompletedFoxSemidirectKernelWordPoint_left
(φ : X → H) (w : FreeGroup X) :
(freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w).left =
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) wThe left coordinate of a completed Fox semidirect kernel-word point is its completed Fox derivative vector.
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\). 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. 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. 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 freeProCZCCompletedFoxSemidirectKernelWordPoint_right
(φ : X → H) (w : FreeGroup X) :
(freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w).right = 1The right coordinate of a completed Fox semidirect kernel-word point is the identity element.
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\). 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. 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. 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 freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
(φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w ∈
freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φA genuine kernel word gives an element of the algebraic kernel-word cycle set.
Show proof
by
exact ⟨w, hw, rfl⟩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. 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. 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 mem_freeProCZCCompletedFoxSemidirectKernelCycleSet_iff
(φ : X → H)
(y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
y ∈ freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ ↔
∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
y = freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ wMembership in the completed Fox semidirect kernel-cycle set is equivalent to vanishing of the corresponding finite-stage coordinate.
Show proof
by
constructor
· intro hy
rcases hy with ⟨w, hw, hy⟩
exact ⟨w, hw, hy⟩
· rintro ⟨w, hw, hy⟩
rw [hy]
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. 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. 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 freeProCZCCompletedFoxSemidirectBoundaryCycleSet_mk_iff
[Fintype X] (φ : X → H)
(v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) :
({ left := v, right := (1 : H) } :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) ∈
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ↔
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v = 0Boundary-cycle membership for a point of the form \((v,1)\).
Show proof
by
constructor
· intro h
exact h.2
· intro h
exact ⟨rfl, h⟩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. 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. 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_quotKernel_approx
[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) π)
(happrox :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ j : J,
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
π j (freeProCZCCompletedFoxSemidirectKernelWordPoint
(ProC := ProC) φ w) = π j y) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Quotient-kernel approximation form of the completed Fox density statement. This is the finite-stage attack surface for the remaining density theorem: once finite quotient exactness produces, for every finite quotient stage j, a kernel word whose semidirect point has the same j-th quotient image as the boundary cycle, the completed density statement follows.
Show proof
by
refine subset_closure_of_quotientKernel_approximation
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(S := freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)
(T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)
π hbasis ?_
intro y hy j
rcases happrox y hy j with ⟨w, hw, hπ⟩
exact
⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w,
freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
(ProC := ProC) φ hw,
hπ⟩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_open_neighbourhood_approx
[Fintype X] (φ : X → H)
(happrox :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ U : Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
IsOpen U → y ∈ U →
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w ∈ U) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Neighborhood approximation form of the completed Fox density statement. For every boundary cycle and every open neighborhood of it in the completed semidirect product, there is a genuine kernel word whose point \((D w, 1)\) lies in that neighborhood. This proves the set-level density statement used by the Crowell middle exactness theorem.
Show proof
by
refine subset_closure_of_open_neighbourhood_approximation ?_
intro y hy U hU hyU
rcases happrox y hy U hU hyU with ⟨w, hw, hUmem⟩
refine ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w, ?_, hUmem⟩
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_openSubgroup_approx
[Fintype X] (φ : X → H)
(hbasis :
HasLeftOpenSubgroupNeighbourhoodBasis
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(happrox :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
IsOpen ((V : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
(ProC := ProC) φ w ∈ V) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Open-subgroup approximation form of the completed Fox density statement. This is the intended entry point for finite quotient arguments: for every open subgroup V of the completed Fox semidirect group, approximate a boundary cycle y by a kernel-word cycle point modulo the left coset y V.
Show proof
by
refine subset_closure_of_openSubgroup_approximation
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(S := freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)
(T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)
hbasis ?_
intro y hy V hVopen
rcases happrox y hy V hVopen with ⟨w, hw, hVmem⟩
exact
⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w,
freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
(ProC := ProC) φ hw,
hVmem⟩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. 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_openNormalSubgroup_approx
[Fintype X] (φ : X → H)
(hbasis :
HasLeftOpenNormalSubgroupNeighbourhoodBasis
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(happrox :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
V.Normal →
IsOpen ((V : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
(ProC := ProC) φ w ∈ V) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)Open-normal-subgroup approximation form of the completed Fox density statement.
Show proof
by
refine subset_closure_of_openNormalSubgroup_approximation
(Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(S := freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)
(T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)
hbasis ?_
intro y hy V hVnormal hVopen
rcases happrox y hy V hVnormal hVopen with ⟨w, hw, hVmem⟩
exact
⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w,
freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
(ProC := ProC) φ hw,
hVmem⟩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. 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_openSubgroup_approx
[Fintype X] (φ : X → H)
(hbasis :
HasLeftOpenSubgroupNeighbourhoodBasis
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(happrox :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
IsOpen ((V : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
(ProC := ProC) φ w ∈ V) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Open-subgroup approximation places every completed boundary cycle inside the closed generated Fox graph target.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx
(ProC := ProC) φ hbasis happrox)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\). 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 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 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openNormalSubgroup_approx
[Fintype X] (φ : X → H)
(hbasis :
HasLeftOpenNormalSubgroupNeighbourhoodBasis
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(happrox :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
V.Normal →
IsOpen ((V : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
(ProC := ProC) φ w ∈ V) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Open-normal-subgroup approximation places every completed boundary cycle inside the closed generated Fox graph target.
Show proof
by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
(ProC := ProC) φ
(freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openNormalSubgroup_approx
(ProC := ProC) φ hbasis happrox)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\). 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 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 closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_of_openSubgroup_approx
[Fintype X] [T1Space H]
[TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
[T1Space (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
(φ : X → H)
(hleft :
Continuous
(fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.left))
(hright :
Continuous
(fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.right))
(hboundary :
Continuous
(zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ)))
(hbasis :
HasLeftOpenSubgroupNeighbourhoodBasis
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(happrox :
∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ →
∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
IsOpen ((V : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
∃ w : FreeGroup X,
FreeGroup.lift φ w = 1 ∧
y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
(ProC := ProC) φ w ∈ V) :
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) =
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φUnder the standard continuity inputs, open-subgroup approximation upgrades the one-sided closure statement to the equality between boundary cycles and the closure of kernel-word cycles.
Show proof
by
exact
(closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density
(ProC := ProC) φ hleft hright hboundary).2
(freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx
(ProC := ProC) φ hbasis happrox)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. 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.
□