FoxDifferential.Completed.FreeProC.SemidirectLift
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def freeProCZCCompletedFoxSemidirectGenerator (φ : X → H) :
X → ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
fun x =>
{ left := Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
right := φ x }The generator map into the completed Fox semidirect target attached to a basis-value map \(\varphi: X \to H\).
theorem freeProCZCCompletedFoxSemidirectGenerator_left
(φ : X → H) (x : X) :
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The generator map has the expected left coordinate.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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 freeProCZCCompletedFoxSemidirectGenerator_right
(φ : X → H) (x : X) :
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x).right = φ xThe generator map has the expected right coordinate.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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 freeProCZCCompletedFoxSemidirectGenerator_convergesToOne_of_finite
[Finite X] (φ : X → H) :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)Show proof
by
exact FamilyConvergesToOne.of_finite_domain
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)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\). 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.
□def freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (φ : X → H) :
ClosedSubgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
ProCGroups.Generation.closedSubgroupGenerated
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))The closed subgroup of the completed Fox semidirect target generated by the Fox graph generators.
theorem freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_proCGroup
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients]
[ProCGroups.ProC.ProCGroup ProC
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
(φ : X → H) :
ProCGroups.ProC.ProCGroup ProC
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))If the ambient completed Fox semidirect target is a pro-\(C\) group, then the closed target generated by the Fox graph generators is pro-\(C\) by closed-subgroup permanence.
Show proof
ProCGroups.ProC.ProCGroup.of_closedSubgroup ProC
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (ProC := ProC) φ)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 freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_proC
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients]
[ProCGroups.ProC.ProCGroup ProC
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
(φ : X → H) :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))The closed generated target of the free pro-\(C\), \(\mathbb{Z}_C\)-completed Fox semidirect construction is a pro-\(C\) group.
Show proof
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_proCGroup
(ProC := ProC) φ).isProCProof. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (φ : X → H) :
X →
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
ProCGroups.Generation.closedSubgroupGeneratedMap
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)The Fox graph generator map, with codomain restricted to the closed subgroup it generates.
theorem freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val
(φ : X → H) (x : X) :
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ x :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xThe closed-generated Fox semidirect generator has underlying value equal to the corresponding semidirect generator.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget
(φ : X → H) (x : X) :
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x ∈
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Each Fox graph generator belongs to the closed subgroup generated by the Fox graph.
Show proof
by
simpa using
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ x).2Proof. 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 zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget
(φ : X → H) (w : FreeGroup X) :
zcCompletedFoxSemidirectLift ProC.finiteQuotientClass (FreeGroup.lift φ) w ∈
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))The completed semidirect Fox graph of every abstract free-group word lies in the closed subgroup generated by the Fox graph generators.
Show proof
by
induction w using FreeGroup.induction_on with
| C1 =>
simp only [map_one, one_mem]
| of x =>
have hpoint :
zcCompletedFoxSemidirectLift ProC.finiteQuotientClass
(FreeGroup.lift φ) (FreeGroup.of x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
simp only [zcCompletedFoxSemidirectLift, FreeGroup.lift_apply_of, freeProCZCCompletedFoxSemidirectGenerator]
rw [hpoint]
exact
freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget
(ProC := ProC) φ x
| inv_of x hx =>
simpa [map_inv] using
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)).inv_mem hx
| mul u v hu hv =>
simpa [map_mul] using
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)).mul_mem hu hvProof. 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 freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
(φ : X → H) (w : FreeGroup X) :
({ left :=
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
right := FreeGroup.lift φ w } :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) ∈
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Equivalently, the pair consisting of the completed free Fox derivative vector and the target word value belongs to the closed generated Fox graph.
Show proof
by
simpa [zcCompletedFoxSemidirectLift_eq] using
zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget
(ProC := ProC) φ wProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. 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. 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 freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel
(φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
({ left :=
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
right := (1 : H) } :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) ∈
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))If an abstract free-group word maps trivially to the target group, its completed Fox derivative vector gives a genuine cycle point \((D w, 1)\) in the closed generated Fox graph.
Show proof
by
simpa [hw] using
freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
(ProC := ProC) φ wProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def freeProCZCCompletedFoxSemidirectKernelCycleSet (φ : X → H) :
Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
{ y | ∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
y =
({ left :=
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift φ) w,
right := (1 : H) } :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) }The algebraic kernel-word cycle points in the completed Fox semidirect product. These are the points \((D w, 1)\) obtained from abstract free-group words whose target value is 1. The remaining density step for the completed Fox cycles is formulated using the closure of this set.
def freeProCZCCompletedFoxSemidirectBoundaryCycleSet [Fintype X] (φ : X → H) :
Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
{ y | y.right = 1 ∧
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) y.left = 0 }The completed Fox boundary-cycle set inside the completed Fox semidirect product. Its points are exactly the pairs \((v,1)\) whose coordinate vector is killed by the source-shaped completed Fox boundary. The remaining density step can be expressed as saying that this boundary-cycle set is contained in the closure of the algebraic kernel-word cycle set.
def freeProCZCCompletedFoxSemidirectGraphWordPoint (φ : X → H) (w : FreeGroup X) :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
{ left :=
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
right := FreeGroup.lift φ w }The genuine completed Fox graph point \((D w, \varphi(w))\) attached to an abstract free-group word.
theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_left
(φ : X → H) (w : FreeGroup X) :
(freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w).left =
zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) wThe left component of a semidirect graph-word point is the completed free-group Fox derivative vector of the word.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_right
(φ : X → H) (w : FreeGroup X) :
(freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w).right =
FreeGroup.lift φ wThe right component of a semidirect graph-word point is \(\mathrm{FreeGroup.lift}(\varphi)(w)\).
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□def freeProCZCCompletedFoxSemidirectGraphWordSet (φ : X → H) :
Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
{ y | ∃ w : FreeGroup X,
y = freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w }The set of all completed Fox graph points attached to abstract free-group words.
theorem mem_freeProCZCCompletedFoxSemidirectGraphWordSet_iff
(φ : X → H)
(y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
y ∈ freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ ↔
∃ w : FreeGroup X,
y = freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ wMembership in the completed Fox semidirect graph word set is equivalent to the displayed coordinate condition.
Show proof
by
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget
(φ : X → H) (w : FreeGroup X) :
freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w ∈
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Every completed graph-word point lies in the closed subgroup generated by the Fox graph generators.
Show proof
by
simpa [freeProCZCCompletedFoxSemidirectGraphWordPoint] using
freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
(ProC := ProC) φ wProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. 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 freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget
(φ : X → H) :
freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))The graph-word set lies in the closed subgroup generated by the Fox graph generators.
Show proof
by
rintro y ⟨w, rfl⟩
exact freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget
(ProC := ProC) φ wProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). 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 closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget
(φ : X → H) :
closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ) ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))The closure of the graph-word set remains in the closed generated Fox graph target.
Show proof
closure_minimal
(freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget
(ProC := ProC) φ)
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (ProC := ProC) φ).isClosed'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. 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_closedGenTarget_of_graphWord_density
[Fintype X] (φ : X → H)
(hdensity :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ)) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Graph-word density places every completed boundary cycle in the closed generated Fox graph target.
Show proof
by
exact subset_trans hdensity
(closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget
(ProC := ProC) φ)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. 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 zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel
[Fintype X] (φ : X → H) {w : FreeGroup X}
(hw : FreeGroup.lift φ w = 1) :
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ)
(zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w) = 0A kernel word has zero completed Fox boundary. This is the completed Fox fundamental formula applied before taking closures: if \(w\) maps to \(1\), then the Euler boundary of its Fox derivative vector is zero.
Show proof
by
rw [zcFreeGroupFoxBoundary_derivativeVector]
exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
(C := ProC.finiteQuotientClass) (ψ := FreeGroup.lift φ) 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. 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 freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
[Fintype X] (φ : X → H) :
freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ ⊆
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φEvery algebraic kernel-word cycle point is an actual completed Fox boundary cycle.
Show proof
by
intro y hy
rcases hy with ⟨w, hw, rfl⟩
constructor
· rfl
· exact zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel
(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.
□def freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
[Fintype X] (φ : X → H) :
Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) where
carrier := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ
one_mem' := by
constructor
· rfl
· simp only [ZCCompletedFoxSemidirect.one_left, map_zero]
mul_mem' := by
intro a b ha hb
rcases ha with ⟨ha_right, ha_boundary⟩
rcases hb with ⟨hb_right, hb_boundary⟩
constructor
· simp only [ZCCompletedFoxSemidirect.mul_right, ha_right, hb_right, mul_one]
· calc
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) (a * b).left
= zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ)
(a.left + b.left) := by
simp only [ZCCompletedFoxSemidirect.mul_left, ha_right, map_one, one_smul, map_add]
_ = zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) a.left +
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) b.left := by
rw [map_add]
_ = 0 := by
simp only [ha_boundary, hb_boundary, add_zero]
inv_mem' := by
intro a ha
rcases ha with ⟨ha_right, ha_boundary⟩
constructor
· simp only [ZCCompletedFoxSemidirect.inv_right, ha_right, inv_one]
· calc
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) a⁻¹.left
= zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) (-a.left) := by
simp only [ZCCompletedFoxSemidirect.inv_left, ha_right, inv_one, map_one, one_smul, map_neg]
_ = -zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) a.left := by
rw [map_neg]
_ = 0 := by
simp only [ha_boundary, neg_zero]The boundary-cycle points form an actual subgroup of the completed Fox semidirect product. Algebraically this is the additive kernel of the source-shaped completed Fox boundary, embedded as the right-trivial subgroup \((v,1)\).
theorem freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup_coe
[Fintype X] (φ : X → H) :
((freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) =
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φThe \(\mathbb{Z}_C\)-completed differential-module boundary is the finite-stage boundary obtained from the source and target coordinates.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous
[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 φ))) :
IsClosed (freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ)The completed Fox boundary-cycle set is closed whenever the two semidirect projections and the source-shaped completed Fox boundary are continuous. This is the topological half of the density frontier: algebraic kernel-word cycles stay inside actual boundary cycles after taking closure.
Show proof
by
have hright_closed :
IsClosed
((fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.right) ⁻¹'
({1} : Set H)) :=
isClosed_singleton.preimage hright
have hboundary_closed :
IsClosed
((fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H =>
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) y.left) ⁻¹'
({0} : Set (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))) :=
isClosed_singleton.preimage (hboundary.comp hleft)
simpa [freeProCZCCompletedFoxSemidirectBoundaryCycleSet] using
hright_closed.inter hboundary_closedProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous
[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 φ))) :
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) ⊆
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φClosure of algebraic kernel-word cycle points remains inside the actual completed Fox boundary-cycle set, assuming the displayed boundary-cycle set is topologically closed.
Show proof
by
exact
closure_minimal
(freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
(ProC := ProC) φ)
(isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous
(ProC := ProC) φ hleft hright hboundary)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. 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 closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density
[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 φ))) :
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) =
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ↔
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)With the continuity inputs in place, the remaining density statement is equivalently the claim that the closure of algebraic kernel-word cycle points is exactly the boundary-cycle set.
Show proof
by
constructor
· intro h y hy
simpa [h] using hy
· intro hdensity
ext y
constructor
· intro hy
exact
closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous
(ProC := ProC) φ hleft hright hboundary hy
· intro hy
exact hdensity hyProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). 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 freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget
(φ : X → H) :
freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Every algebraic kernel-word cycle point lies in the closed generated Fox graph target.
Show proof
by
intro y hy
rcases hy with ⟨w, hw, rfl⟩
exact
freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel
(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. 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. 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 closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
(φ : X → H) :
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))The closure of algebraic kernel-word cycle points is still contained in the closed generated Fox graph target.
Show proof
by
exact
closure_minimal
(freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget
(ProC := ProC) φ)
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (ProC := ProC) φ).isClosed'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. 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_closedGenTarget_of_density
[Fintype X] (φ : X → H)
(hdensity :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))If the boundary-cycle set is dense in the algebraic kernel-word closure, then every completed Fox boundary cycle belongs to the closed subgroup generated by the Fox graph.
Show proof
by
intro y hy
exact
closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
(ProC := ProC) φ (hdensity hy)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 freeProCZCFoxClosedGenTarget_mem_of_mem_closure_kernelCycleSet
(φ : X → H)
{y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
(hy :
y ∈ closure
(freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)) :
y ∈
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))Pointwise form of the closure step for algebraic kernel-word cycle points.
Show proof
closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
(ProC := ProC) φ hyProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). 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 freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
(φ : X → H) :
ProCGroups.Generation.TopologicallyGenerates
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(Set.range
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))The restricted Fox graph generators topologically generate their closed generated target.
Show proof
ProCGroups.Generation.closedSubgroupGeneratedMap_topologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)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. 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 freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
[Finite X] (φ : X → H) :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)Show proof
by
exact FamilyConvergesToOne.of_finite_domain
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
F →*
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
hι.lift htarget
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)
hφconv
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
(ProC := ProC) φ)The completed Fox semidirect lift into the closed target generated by the graph generators. This is the converging-set version needed when the graph generators do not generate the whole semidirect product.
def freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
F →ₜ*
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
hι.liftHom htarget
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)
hφconv
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
(ProC := ProC) φ)Continuous homomorphism form of the closed-generated semidirect lift.
theorem freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_toMonoidHom
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
(freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
(ProC := ProC) hι φ htarget hφconv).toMonoidHom =
freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
(ProC := ProC) hι φ htarget hφconvForgetting continuity from the closed-generated semidirect lift homomorphism recovers the underlying closed-generated semidirect lift.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
(ProC := ProC) hι φ htarget hφconv (ι x) =
freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ xThe closed-generated semidirect lift sends each free pro-\(C\) generator to the corresponding closed-generated Fox semidirect generator.
Show proof
(hι.lift_spec htarget
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)
hφconv
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
(ProC := ProC) φ)).2 xProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective
[CompactSpace F]
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
[T2Space
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))]
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
Function.Surjective
(freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
(ProC := ProC) hι φ htarget hφconv)The closed-generated semidirect lift is surjective onto the closed target generated by the Fox graph generators. This is the mathematically valid replacement for the generally false claim that the Fox graph generators fill the whole completed semidirect product: the universal map from the free pro-\(C\) group is onto exactly the closed subgroup generated by those graph generators.
Show proof
by
refine
ProCGroups.Generation.continuousMonoidHom_surjective_of_topologicallyGenerates_subset_range
(f := freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
(ProC := ProC) hι φ htarget hφconv)
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
(ProC := ProC) φ) ?_
rintro y ⟨x, rfl⟩
refine ⟨ι x, ?_⟩
change
freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
(ProC := ProC) hι φ htarget hφconv (ι x) =
freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ x
exact freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator
(ProC := ProC) hι φ htarget hφconv xProof. 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. Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. 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. 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 freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)).subtype.comp
(freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
(ProC := ProC) hι φ htarget hφconv)The lift through the closed generated subgroup, composed with the inclusion into the full completed Fox semidirect product.
theorem freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget
[CompactSpace F]
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
[T2Space
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))]
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
{y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
(hy : y ∈
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))) :
∃ g : F,
freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv g = yElementwise form of the semidirect lift theorem, formulated in the ambient completed Fox semidirect product. Every element of the closed Fox graph target has a preimage under the free pro-\(C\) semidirect lift.
Show proof
by
let yclosed :
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
⟨y, hy⟩
rcases
freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective
(ProC := ProC) hι φ htarget hφconv yclosed with
⟨g, hg⟩
refine ⟨g, ?_⟩
simpa [freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated, yclosed] using
congrArg Subtype.val hgProof. 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. 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 freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv (ι x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xThe closed-generated semidirect lift into the ambient semidirect product sends each free pro-\(C\) generator to the corresponding Fox semidirect generator.
Show proof
by
simp only [freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated, MonoidHom.coe_comp, Subgroup.coe_subtype,
Function.comp_apply, freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator,
freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val]Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def freeProCZCCompletedFoxRightHomViaClosedGenerated
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
F →* H :=
(ZCCompletedFoxSemidirect.rightMonoidHom ProC.finiteQuotientClass X H).comp
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv)The right component of the closed-generated semidirect lift.
theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_generator
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv (ι x) = φ xThe right component of the closed-generated semidirect lift sends each generator to its prescribed value \(\varphi(x)\).
Show proof
by
simp only [freeProCZCCompletedFoxRightHomViaClosedGenerated, MonoidHom.coe_comp, Function.comp_apply,
freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator, ZCCompletedFoxSemidirect.rightMonoidHom_apply,
freeProCZCCompletedFoxSemidirectGenerator_right]Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
(g : F) :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv g).leftThe derivative-vector component of the closed-generated semidirect lift.
theorem freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The derivative-vector component of the closed-generated semidirect lift has standard basis value at each generator.
Show proof
by
simp only [freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated,
freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator, freeProCZCCompletedFoxSemidirectGenerator_left]Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_isCrossedDifferential
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv))
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv)The closed-generated derivative vector is a crossed differential with respect to its right component.
Show proof
by
intro g h
have hmul := congrArg ZCCompletedFoxSemidirect.left
(map_mul
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv) g h)
change
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv (g * h)).left =
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv g).left +
zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv) g •
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv h).left
rw [hmul]
simp only [ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHomViaClosedGenerated,
zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp, Function.comp_apply,
ZCCompletedFoxSemidirect.rightMonoidHom_apply]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. 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.
□def freeProCZCCompletedFoxSemidirectLift
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφThe continuous completed Fox semidirect lift from a free pro-\(C\) source.
def freeProCZCCompletedFoxSemidirectLiftHom
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφThe continuous homomorphism form of the completed Fox semidirect lift from a free pro-\(C\) source.
theorem freeProCZCCompletedFoxSemidirectLiftHom_toMonoidHom
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
(freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφ).toMonoidHom =
freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφForgetting continuity from the continuous semidirect lift gives the underlying semidirect lift.
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\). 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. 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 continuous_freeProCZCCompletedFoxSemidirectLift
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
Continuous (freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ)The free pro-\(C\) semidirect lift is continuous.
Show proof
(freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφ).continuous_toFunProof. 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. 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 freeProCZCCompletedFoxSemidirectLift_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ (ι x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xThe free pro-\(C\) semidirect lift has the prescribed completed Fox generator values.
Show proof
(hι.lift_spec htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ).2 xProof. 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. 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□theorem freeProCZCCompletedFoxSemidirectLiftHom_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφ (ι x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xThe continuous semidirect lift has the prescribed completed Fox generator values.
Show proof
hι.liftHom_apply htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ xProof. 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. 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.
□def freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
hφconv hφgendef freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
hφconv hφgenContinuous homomorphism form of the converging-set completed Fox semidirect lift.
theorem freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_toMonoidHom
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
(freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen).toMonoidHom =
freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgenForgetting continuity from the converging-set semidirect lift homomorphism gives the unbundled lift.
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\). 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□theorem continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
Continuous (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)The completed Fox semidirect lift associated to a converging generator family is continuous.
Show proof
(freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen).continuous_toFunProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. 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 freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
(x : X) :
freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen (ι x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xThe converging-set semidirect lift has the prescribed generator values.
Show proof
(hι.lift_spec htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
hφconv hφgen).2 xProof. 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. 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□theorem freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_surjective
[CompactSpace F]
[T2Space (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
Function.Surjective
(freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)The converging-set semidirect lift is surjective once its prescribed generator values topologically generate the semidirect target.
Show proof
by
refine
ProCGroups.Generation.continuousMonoidHom_surjective_of_topologicallyGenerates_subset_range
(f := freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)
hφgen ?_
rintro y ⟨x, rfl⟩
refine ⟨ι x, ?_⟩
change
freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen (ι x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x
exact freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator
(ProC := ProC) hι htarget φ hφconv hφgen xProof. 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\). Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. 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.
□def freeProCZCCompletedFoxRightHomOfConvergingSet
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
F →* H :=
(ZCCompletedFoxSemidirect.rightMonoidHom ProC.finiteQuotientClass X H).comp
(freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)The right component of the converging-set semidirect lift.
def freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
(g : F) :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
(freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen g).leftThe derivative-vector component of the converging-set semidirect lift.
theorem freeProCZCCompletedFoxRightHomOfConvergingSet_generator
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
(x : X) :
freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen (ι x) = φ xThe right component of the converging-set semidirect lift sends each generator to its prescribed value \(\varphi(x)\).
Show proof
by
simp only [freeProCZCCompletedFoxRightHomOfConvergingSet, MonoidHom.coe_comp, Function.comp_apply,
freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator, ZCCompletedFoxSemidirect.rightMonoidHom_apply,
freeProCZCCompletedFoxSemidirectGenerator_right]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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
(x : X) :
freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The derivative-vector component of the converging-set semidirect lift has standard basis value at each generator.
Show proof
by
simp only [freeProCZCCompletedFoxDerivativeVectorOfConvergingSet,
freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator, freeProCZCCompletedFoxSemidirectGenerator_left]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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_isCrossedDifferential
{ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen))
(freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)The converging-set derivative vector is a crossed differential with respect to its right component.
Show proof
by
intro g h
change
(freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen (g * h)).left =
(freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen g).left +
zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen) g •
(freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen h).left
simp only [map_mul, ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHomOfConvergingSet,
ZCCompletedFoxSemidirect.rightMonoidHom, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp, MonoidHom.coe_mk,
OneHom.coe_mk, Function.comp_apply]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. 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□def freeProCZCCompletedFoxSemidirectLiftMorphism
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
ProCGrp.of ProC F ⟶
ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
hι.liftMorphism
(ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφThe categorical completed Fox semidirect lift from a free pro-\(C\) source is bundled as a morphism in ProCGrp.
theorem freeProCZCCompletedFoxSemidirectLiftMorphism_hom
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
(freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ).hom =
freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι
(inferInstanceAs
(ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
φ hφThe underlying continuous homomorphism of the categorical completed Fox semidirect lift is the free pro-\(C\) continuous homomorphism supplied by liftHom.
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\). 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 freeProCZCCompletedFoxSemidirectLiftMorphism_hom_toMonoidHom
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
(freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ).hom.toMonoidHom =
freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι
(inferInstanceAs
(ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
φ hφThe underlying homomorphism of the categorical completed Fox semidirect lift is the unbundled completed Fox semidirect lift.
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\). 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 freeProCZCCompletedFoxSemidirectLiftMorphism_generator
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ (ι x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xThe categorical completed Fox semidirect lift has the prescribed generator values.
Show proof
hι.liftMorphism_apply
(ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ xProof. 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\). 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 freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
(freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The left component of the categorical completed Fox semidirect lift has the standard Fox coordinate on each generator.
Show proof
by
rw [freeProCZCCompletedFoxSemidirectLiftMorphism_generator]
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
(freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ (ι x)).right = φ xThe right component of the categorical completed Fox semidirect lift has the prescribed generator value.
Show proof
by
rw [freeProCZCCompletedFoxSemidirectLiftMorphism_generator]
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\). 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 freeProCZCCompletedFoxSemidirectLift_left_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The left component of the free pro-\(C\) semidirect lift has the standard Fox coordinate on each generator.
Show proof
by
rw [freeProCZCCompletedFoxSemidirectLift_generator]
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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 freeProCZCCompletedFoxSemidirectLiftHom_left_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
(freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφ (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The left component of the continuous free pro-\(C\) semidirect lift has the standard Fox coordinate on each generator.
Show proof
by
rw [freeProCZCCompletedFoxSemidirectLiftHom_generator]
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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 freeProCZCCompletedFoxSemidirectLift_right_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ (ι x)).right = φ xThe right component of the free pro-\(C\) semidirect lift has the prescribed generator value.
Show proof
by
rw [freeProCZCCompletedFoxSemidirectLift_generator]
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\). 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□theorem freeProCZCCompletedFoxSemidirectLiftHom_right_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
(freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφ (ι x)).right = φ xThe right component of the continuous free pro-\(C\) semidirect lift has the prescribed generator value.
Show proof
by
rw [freeProCZCCompletedFoxSemidirectLiftHom_generator]
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\). 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. 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.
□def freeProCZCCompletedFoxRightHom
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
F →* H where
toFun g := (freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ g).right
map_one' := by
simp only [map_one, ZCCompletedFoxSemidirect.one_right]
map_mul' g h := by
simp only [map_mul, ZCCompletedFoxSemidirect.mul_right]The target-group component of the continuous completed Fox semidirect lift.
theorem freeProCZCCompletedFoxRightHom_apply
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(g : F) :
freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ g =
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ g).rightThe right component of the continuous completed Fox semidirect lift is the associated homomorphism.
Show proof
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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 freeProCZCCompletedFoxRightHom_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ (ι x) = φ xThe target-group component has the prescribed generator values.
Show proof
by
rw [freeProCZCCompletedFoxRightHom_apply,
freeProCZCCompletedFoxSemidirectLift_right_generator]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. 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. The Fox-specific step is the fundamental identity expressing an element minus its augmentation as the sum of its Fox derivatives multiplied by the corresponding generator increments. This identity identifies the relevant augmentation kernel with the image or closed span generated by the displayed differential coordinates.
□def freeProCZCCompletedFoxDerivativeVector
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(g : F) :
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ g).leftThe completed Fox derivative vector is obtained as the left component of the continuous free pro-\(C\) semidirect lift.
theorem freeProCZCCompletedFoxDerivativeVector_generator
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(x : X) :
freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)The free pro-\(C\) completed Fox derivative vector has the standard coordinate value on generators.
Show proof
by
rw [freeProCZCCompletedFoxDerivativeVector,
freeProCZCCompletedFoxSemidirectLift_left_generator]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. 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 freeProCZCCompletedFoxDerivativeVector_isCrossedDifferential
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ))
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ)The free pro-\(C\) completed Fox derivative vector is a crossed differential with respect to the target-group component of the continuous semidirect lift.
Show proof
by
intro g h
have hmul := congrArg ZCCompletedFoxSemidirect.left
(map_mul (freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ) g h)
change (freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ (g * h)).left =
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ g).left +
zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
(freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ) g •
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ h).left
rw [hmul]
simp only [ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHom,
zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_mk, OneHom.coe_mk]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. 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.
□