The separated completed Crowell sequence

Mathematical statement

Let $C$ satisfy the source’s full-formation assumptions and contain trivial quotients. The formation package includes closure under quotients, finite subdirect products, normal subgroups, extensions, and subgroups. Let $F$ be a free pro-$C$ group with a chosen converging basis of finite cardinality $r$, and let $\psi:F\twoheadrightarrow H$ be a continuous surjection to a profinite group.

For $N=\ker\psi$, the separated completed differential module gives $$0\to N/\overline{[N,N]}\to A^{\mathrm{sep}}_\psi(C)\to\mathbb Z_C\mathopen{[\![} H\mathclose{]\!]}\to\mathbb Z_C\to0.$$ The bundled endpoint records exactness of the underlying integer-linear maps.

Here $\mathbb Z_C$ is the pro-$C$ completion of the additive group $\mathbb Z$, with its induced ring structure, and $\mathbb Z_C\mathopen{[\![} H\mathclose{]\!]}$ is the corresponding completed group algebra.

Lean code

`CrowellExactSequence.freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj`

Published library source ↗Same source in NYLL ↗

theorem freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
    [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) :
    Function.Injective
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := sourceData.carrier) (H := H) C psi) ∧
      Function.Exact
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := sourceData.carrier) (H := H) C psi)
        (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
          (G := sourceData.carrier) (H := H) C
          hC.hereditary psi) ∧
        Function.Exact
          (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
            (G := sourceData.carrier) (H := H) C
            hC.hereditary psi)
          (zcCompletedGroupAlgebraAugmentation C H) ∧
          Function.Surjective
            (zcCompletedGroupAlgebraAugmentation C H)

In-scope Lean context

namespace CrowellExactSequence

noncomputable section

open FoxDifferential

open ProCGroups.ProC

universe u

variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

variable {C : ProCGroups.FiniteGroupClass.{u}}

variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]

Full declaration and proof

/--
The all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the separated
Crowell exact sequence over \(\mathbb{Z}_C\).
-/
theorem freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
    [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) :
    Function.Injective
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := sourceData.carrier) (H := H) C psi) ∧
      Function.Exact
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := sourceData.carrier) (H := H) C psi)
        (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
          (G := sourceData.carrier) (H := H) C
          hC.hereditary psi) ∧
        Function.Exact
          (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
            (G := sourceData.carrier) (H := H) C
            hC.hereditary psi)
          (zcCompletedGroupAlgebraAugmentation C H) ∧
          Function.Surjective
            (zcCompletedGroupAlgebraAugmentation C H) :=
by
  exact
    ⟨freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
        (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi,
      freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
        (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi,
      freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
        (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi,
      zcCompletedGroupAlgebraAugmentation_surjective
        (C := C) (H := H)⟩

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Luis Ribes and Pavel Zalesskii. Profinite Groups. Springer-Verlag Berlin Heidelberg, 2010. Second edition; Ergebnisse der Mathematik und ihrer Grenzgebiete, 3. Folge, volume 40.
R. H. Crowell. The Derived Module of a Homomorphism. Advances in Mathematics, 6, 210–238, 1971. Original article; the linked PDF reproduces the published text.