CrowellExactSequence/Discrete/MainTheorem.lean
1import CrowellExactSequence.Discrete.BlanchfieldLyndon
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CrowellExactSequence/Discrete/MainTheorem.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete Crowell main theorems
14This file is the paper-facing entry point for the discrete main statements. The conclusions
15are packaged as four-term exact sequences, not as isolated surjectivity or middle-exactness
16lemmas.
17-/
19namespace CrowellExactSequence
21noncomputable section
23open FoxDifferential
25variable {H : Type} [Group H]
27/-- The discrete Crowell exact sequence for a surjective group homomorphism, packaged as the
28full four-term exact sequence
30theorem discreteCrowellExactSequence
31 {G : Type} [Group G]
32 (psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
33 letI := kernelAbelianizationModuleOfSurjective psi hpsi
35 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
36 (toGroupRing psi)
37 (augmentation H) := by
38 letI := kernelAbelianizationModuleOfSurjective psi hpsi
39 exact Morishita2024.crowellExactSequence_of_surjective (H := H) psi hpsi
41/-- The discrete Blanchfield--Lyndon coordinate exact sequence for a finite free presentation,
42packaged as the full four-term exact sequence. -/
44 (r : Nat) (psi : MonoidHom (FreeGroup (Fin r)) H) (hpsi : Function.Surjective psi) :
45 letI := kernelAbelianizationModuleOfSurjective psi hpsi
47 (FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi)
48 (FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi)
49 (augmentation H) := by
50 letI := kernelAbelianizationModuleOfSurjective psi hpsi
51 exact Morishita2024.freeGroupPresentation_blanchfieldLyndonExactSequence (H := H) r psi hpsi
53end
55end CrowellExactSequence