The discrete Crowell exact sequence

Mathematical statement

Let $\psi:G\twoheadrightarrow H$ be a surjective homomorphism of groups and let $N=\ker\psi$. Write $A_\psi$ for the universal module of $\psi$-crossed homomorphisms. Then $$0\longrightarrow N^{\mathrm{ab}}\longrightarrow A_\psi\longrightarrow\mathbb Z[H]\xrightarrow{\varepsilon}\mathbb Z\longrightarrow0$$ is exact.

The head map sends the class of $n$ to its universal differential; the next map sends the differential of $g$ to $[\psi(g)]-1$. The last map is augmentation. The action of $H$ on $N^{\mathrm{ab}}$ comes from conjugation through lifts in $G$.

Lean code

`CrowellExactSequence.Morishita2024.crowellExactSequence_of_surjective`

Published library source ↗Same source in NYLL ↗

theorem crowellExactSequence_of_surjective
    {G : Type} [Group G]
    (psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
    letI := kernelAbelianizationModuleOfSurjective psi hpsi
    Function.Injective
        (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi) ∧
      Function.Exact
        (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
        (toGroupRing psi) ∧
      Function.Exact (toGroupRing psi) (augmentation H) ∧
      Function.Surjective (augmentation H) := by
  let := kernelAbelianizationModuleOfSurjective psi hpsi
  refine ⟨?_, ?_, exact_toGroupRing_augmentation (H := H) psi hpsi,
    augmentation_surjective (H := H)⟩
  · exact FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
      (H := H) (ψ := psi) hpsi
  · exact exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing (H := H) psi hpsi

In-scope Lean context

namespace CrowellExactSequence

noncomputable section

open FoxDifferential

open scoped BigOperators

namespace Morishita2024

variable {H : Type} [Group H]

Full declaration and proof

/-- Discrete Crowell exact sequence for a surjective group homomorphism. -/
theorem crowellExactSequence_of_surjective
    {G : Type} [Group G]
    (psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
    letI := kernelAbelianizationModuleOfSurjective psi hpsi
    Function.Injective
        (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi) ∧
      Function.Exact
        (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
        (toGroupRing psi) ∧
      Function.Exact (toGroupRing psi) (augmentation H) ∧
      Function.Surjective (augmentation H) := by
  let := kernelAbelianizationModuleOfSurjective psi hpsi
  refine ⟨?_, ?_, exact_toGroupRing_augmentation (H := H) psi hpsi,
    augmentation_surjective (H := H)⟩
  · exact FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
      (H := H) (ψ := psi) hpsi
  · exact exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing (H := H) psi hpsi

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

Ralph H. Fox. Free Differential Calculus. I: Derivation in the Free Group Ring. Annals of Mathematics, 57 (3), 547–560, 1953.
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.