CrowellExactSequence.Profinite.ContinuousMagnus.ClosedGeneratedVector
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
def freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(htarget :
ProC
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
sourceData.carrier →
FoxDifferential.ZCFreeFoxCoordinates
ProC.finiteQuotientClass (X := ULift.{u} (Fin r)) (H := H) :=
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let φ : ULift.{u} (Fin r) → H := fun i =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)
let hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(ProC := ProC) φ) :=
FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) φ
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree φ htarget hφconvThe closed-generated continuous Fox derivative vector attached to a finite chosen free pro-\(C\) basis and a presentation map.
theorem freeProC_closedGeneratedTarget_mem_of_freeGroupFoxDerivativeVector_kernel
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
{w : FreeGroup (ULift.{u} (Fin r))}
(hw :
FreeGroup.lift
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) w = 1) :
({ left :=
FoxDifferential.zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
(FreeGroup.lift
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))) w,
right := (1 : H) } :
FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass
(ULift.{u} (Fin r)) H) ∈
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass
(ULift.{u} (Fin r)) H))An abstract kernel word for the chosen finite free basis gives a genuine cycle point in the closed-generated Fox graph target. This is the algebraic source of the completed cycle-lifting step: before passing to closures, every relation word \(w\) with target value \(1\) contributes \((D w, 1)\) to the closed-generated graph.
Show proof
by
exact
FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
hwProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. 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. 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 freeProCCompletedFoxRightHomViaClosedGeneratedProCInteger_eq
[T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
(htarget :
ProC
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
htarget
(FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))) =
psi.toMonoidHomThe right component of the closed-generated Fox graph attached to the chosen lifted finite basis is the original presentation map. This is the target-coordinate half of the paper graph identity. It is independent of the left Fox-coordinate calculation: the right component and psi are continuous homomorphisms from the same free pro-\(C\) group, and they agree on the chosen free generators.
Show proof
by
let X : Type u := ULift.{u} (Fin r)
let ι : X → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree := freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let φ : X → H := fun i => psi (ι i)
let hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(ProC := ProC) φ) :=
FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) φ
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ := by
simpa [φ, ι] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
simpa [φ, ι] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
simpa [X, ι, hfree, φ, hφconv] using
FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
(ProC := ProC) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
(by intro i; rfl)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. 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 freeProCCompletedFoxDerivVecViaClosedGenZC_isCrossedDiff
[T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
(htarget :
ProC
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
FoxDifferential.IsCrossedDifferential
(FoxDifferential.zcCompletedGroupAlgebraScalar
ProC.finiteQuotientClass psi.toMonoidHom)
(freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi htarget)The closed-generated continuous Fox derivative vector is a crossed differential with respect to the original presentation map, once the presentation is surjective.
Show proof
by
let X : Type u := ULift.{u} (Fin r)
let ι : X → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree := freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let φ : X → H := fun i => psi (ι i)
let hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(ProC := ProC) φ) :=
FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) φ
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ := by
simpa [φ, ι] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
simpa [φ, ι] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
have hright :
FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hfree φ htarget hφconv =
psi.toMonoidHom := by
simpa [X, ι, hfree, φ, hφconv] using
freeProCCompletedFoxRightHomViaClosedGeneratedProCInteger_eq
(H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget
have hD :=
FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_isCrossedDifferential
(ProC := ProC) hfree φ htarget hφconv
simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, X, ι, φ,
hfree, hφconv, hright] using hDProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. 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 continuous_freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(htarget :
ProC
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
Continuous
(freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi htarget)The closed-generated continuous Fox derivative vector is continuous.
Show proof
by
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let φ : ULift.{u} (Fin r) → H := fun i =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)
let hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(ProC := ProC) φ) :=
FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) φ
simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, hfree, φ, hφconv] using
FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) (ULift.{u} (Fin r)) H hfree φ htarget hφconvProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. 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. 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 freeProC_zcUnivDiff_kernel_le_closedCommutator_of_closedGenFoxVector
[T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
(htarget :
ProC
(G :=
(FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(FoxDifferential.ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
(hDker :
∀ n : ProfiniteKernelSubgroup psi,
freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi htarget n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
∀ n : ProfiniteKernelSubgroup psi,
FoxDifferential.zcUniversalDifferential
ProC.finiteQuotientClass psi.toMonoidHom n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)Universal completed Magnus-kernel reduction for the closed-generated continuous Fox vector. After this reduction, the remaining paper statement is exactly the concrete continuous Magnus kernel for the completed Fox derivative vector.
Show proof
by
exact
FoxDifferential.zcUniversalDifferential_kernel_le_closedCommutator_of_crossedDifferential
ProC.finiteQuotientClass psi
(freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi htarget)
(freeProCCompletedFoxDerivVecViaClosedGenZC_isCrossedDiff
(H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget)
hDkerProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. 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.
□