ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity

1 Theorem

This module proves injectivity of the completed Magnus map on the abelianized presentation kernel, using the closed-commutator kernel calculation and the general kernel-injectivity criterion.

imports

Imported by

Theorem CrowellExactSequence.freeProC_profKerAbBoundaryAddZC_inj_of_continuousMagnus

omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
theorem freeProC_profKerAbBoundaryAddZC_inj_of_continuousMagnus
    [CompactSpace H]
    [T2Space H]
    [TotallyDisconnectedSpace H]
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
    (htarget :
      HasOpenNormalBasisInClass C
        (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) : Subgroup
            (FoxDifferential.ZCCompletedFoxSemidirect
              C (ULift.{u} (Fin r)) H)))
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger
        (G := sourceData.carrier) (H := H) C psi) :
    Function.Injective
      (profiniteKernelAbelianizationBoundaryAddProCInteger
        (G := sourceData.carrier) (H := H) C 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 Lean proof

ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity

Declarations