CrowellExactSequence/Profinite/MainTheorem.lean
1import CrowellExactSequence.Profinite.BlanchfieldLyndon
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CrowellExactSequence/Profinite/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# Profinite Crowell main theorems
14This file is the paper-facing entry point for the profinite main statements. The conclusions
15are packaged as four-term exact sequences for the separated completed Crowell sequence and its
17-/
19namespace CrowellExactSequence
21noncomputable section
23open FoxDifferential
24open ProCGroups.ProC
26universe u
28variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29variable {ProC : ProCGroupPredicate.{u}}
31variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass]
33/-- The separated completed Crowell exact sequence over pro-`C` integer coefficients, packaged
34as the full four-term exact sequence
35`N^ab(C) -> A_psi(C) -> Z_C[[H]] -> Z_C`. -/
37 [T2Space H]
38 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
39 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
40 [ProC.DeterminedByFiniteQuotients]
41 (sourceData : FreeProCSourceData ProC)
42 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
43 (psi : ContinuousMonoidHom sourceData.carrier H)
44 (hpsi : Function.Surjective psi) :
47 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
49 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
50 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi)
51 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) := by
52 exact
54 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
56/-- The separated completed Blanchfield--Lyndon exact sequence in the universe-lifted finite
57coordinate basis, packaged as the full four-term exact sequence. -/
59 [T2Space H]
60 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
61 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
62 [ProC.DeterminedByFiniteQuotients]
63 (sourceData : FreeProCSourceData ProC)
64 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
65 (psi : ContinuousMonoidHom sourceData.carrier H)
66 (hpsi : Function.Surjective psi) :
69 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
71 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
72 (fun i : ULift.{u} (Fin r) =>
74 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
75 ((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
76 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) := by
77 exact
79 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
81/-- The separated completed Blanchfield--Lyndon exact sequence in the concrete `Fin r`
82coordinate basis, packaged as the full four-term exact sequence. -/
84 [T2Space H]
85 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
86 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
87 [ProC.DeterminedByFiniteQuotients]
88 (sourceData : FreeProCSourceData ProC)
89 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
90 (psi : ContinuousMonoidHom sourceData.carrier H)
91 (hpsi : Function.Surjective psi) :
94 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
96 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
97 (fun i : Fin r =>
99 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
100 ((freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
101 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) := by
102 exact
104 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
106end
108end CrowellExactSequence