CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
theorem freeProC_profKerAbBoundaryAddZC_inj_of_continuousMagnus
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[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))))
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) :
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN)Continuous Magnus injectivity for the displayed boundary \(d_N\): \(N^{\mathrm{ab}}(C)\) \(\to\) \(A_{\psi}(C)\). This step is obtained by combining the completed Fox-vector kernel theorem with the general kernel criterion for the topological kernel abelianization.
Show proof
profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN
(freeProC_zcUnivDiff_kernel_le_closedCommutator_of_closedGenFoxVector
(H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget
(freeProC_closedGeneratedFoxVector_kernel_le_closedCommutator
(H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget))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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. 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.
□