Source: ProCGroups.CrowellExactSequence.Discrete.MainTheorem
1import ProCGroups.CrowellExactSequence.Discrete.Exactness
3/-!
4# Crowell Exact Sequence / Discrete / Main Theorem
6This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed
7coordinate forms.
8-/
10namespace CrowellExactSequence
12noncomputable section
14open FoxDifferential
16variable {H : Type} [Group H]
18/-- The discrete Crowell sequence for a surjective group homomorphism. All three displayed
19maps are bundled as `ℤ`-linear maps so that the source, group-ring, and augmentation terms live
20in one canonical `FourTermLinearSequence`. -/
21def discreteCrowellLinearSequence
22 {G : Type} [Group G]
23 (psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
24 letI := kernelAbelianizationModuleOfSurjective psi hpsi
25 FourTermLinearSequence ℤ
26 (KernelAbelianizationAdd psi) (DifferentialModule psi) (GroupRing H) ℤ := by
27 letI := kernelAbelianizationModuleOfSurjective psi hpsi
28 refine FourTermLinearSequence.ofExact
29 ((kernelAbelianizationBoundaryLinearOfSurjective
30 (H := H) psi hpsi).toAddMonoidHom.toIntLinearMap)
31 ((toGroupRing psi).toAddMonoidHom.toIntLinearMap)
32 ((augmentation H).toAddMonoidHom.toIntLinearMap) ?_
33 rcases Morishita2024.crowellExactSequence_of_surjective (H := H) psi hpsi with
34 ⟨hinj, hhead, hmiddle, hsurj⟩
35 refine ⟨?_, ?_, ?_, ?_⟩
36 · intro x y hxy
37 change kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi x =
38 kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi y at hxy
39 exact hinj hxy
40 · intro y
41 change toGroupRing psi y = 0 ↔
42 ∃ x, kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi x = y
43 exact hhead y
44 · intro y
45 change augmentation H y = 0 ↔ ∃ x, toGroupRing psi x = y
46 exact hmiddle y
47 · intro z
48 rcases hsurj z with ⟨y, hy⟩
49 refine ⟨y, ?_⟩
50 change augmentation H y = z
51 exact hy
53/--
54The discrete Crowell exact sequence for a surjective group homomorphism, packaged as the full
55four-term exact sequence \((\ker \psi)^{\mathrm{ab}} \to A_{\psi} \to \mathbb{Z}[H] \to
56\mathbb{Z}\).
57-/
58@[simp]
59theorem discreteCrowellLinearSequence_isExact
60 {G : Type} [Group G]
61 (psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
62 letI := kernelAbelianizationModuleOfSurjective psi hpsi
63 (discreteCrowellLinearSequence (H := H) psi hpsi).IsExact := by
64 letI := kernelAbelianizationModuleOfSurjective psi hpsi
65 unfold FourTermLinearSequence.IsExact
66 rcases Morishita2024.crowellExactSequence_of_surjective (H := H) psi hpsi with
67 ⟨hinj, hhead, hmiddle, hsurj⟩
68 refine ⟨?_, ?_, ?_, ?_⟩
69 · intro x y hxy
70 change kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi x =
71 kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi y at hxy
72 exact hinj hxy
73 · intro y
74 change toGroupRing psi y = 0 ↔
75 ∃ x, kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi x = y
76 exact hhead y
77 · intro y
78 change augmentation H y = 0 ↔ ∃ x, toGroupRing psi x = y
79 exact hmiddle y
80 · intro z
81 rcases hsurj z with ⟨y, hy⟩
82 refine ⟨y, ?_⟩
83 change augmentation H y = z
84 exact hy
86/-- The discrete Blanchfield--Lyndon sequence in concrete `Fin r` coordinates. -/
87def discreteBlanchfieldLyndonLinearSequence
88 (r : Nat) (psi : MonoidHom (FreeGroup (Fin r)) H) (hpsi : Function.Surjective psi) :
89 letI := kernelAbelianizationModuleOfSurjective psi hpsi
90 FourTermLinearSequence ℤ
91 (KernelAbelianizationAdd psi) (Fin r → GroupRing H) (GroupRing H) ℤ := by
92 letI := kernelAbelianizationModuleOfSurjective psi hpsi
93 refine FourTermLinearSequence.ofExact
94 ((FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap
95 (H := H) r psi hpsi).toAddMonoidHom.toIntLinearMap)
96 ((FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap
97 (H := H) r psi).toAddMonoidHom.toIntLinearMap)
98 ((augmentation H).toAddMonoidHom.toIntLinearMap) ?_
99 rcases
100 Morishita2024.freeGroupPresentation_blanchfieldLyndonExactSequence
101 (H := H) r psi hpsi with
102 ⟨hinj, hhead, hmiddle, hsurj⟩
103 refine ⟨?_, ?_, ?_, ?_⟩
104 · intro x y hxy
105 change
106 FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap
107 (H := H) r psi hpsi x =
108 FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap
109 (H := H) r psi hpsi y at hxy
110 exact hinj hxy
111 · intro y
112 change
113 FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap
114 (H := H) r psi y = 0 ↔
115 ∃ x,
116 FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap
117 (H := H) r psi hpsi x = y
118 exact hhead y
119 · intro y
120 change augmentation H y = 0 ↔
121 ∃ x,
122 FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap
123 (H := H) r psi x = y
124 exact hmiddle y
125 · intro z
126 rcases hsurj z with ⟨y, hy⟩
127 refine ⟨y, ?_⟩
128 change augmentation H y = z
129 exact hy
131/--
132The discrete Blanchfield--Lyndon coordinate exact sequence for a finite free presentation,
133packaged as the full four-term exact sequence.
134-/
135@[simp]
136theorem discreteBlanchfieldLyndonLinearSequence_isExact
137 (r : Nat) (psi : MonoidHom (FreeGroup (Fin r)) H) (hpsi : Function.Surjective psi) :
138 letI := kernelAbelianizationModuleOfSurjective psi hpsi
139 (discreteBlanchfieldLyndonLinearSequence (H := H) r psi hpsi).IsExact := by
140 letI := kernelAbelianizationModuleOfSurjective psi hpsi
141 unfold FourTermLinearSequence.IsExact
142 rcases
143 Morishita2024.freeGroupPresentation_blanchfieldLyndonExactSequence
144 (H := H) r psi hpsi with
145 ⟨hinj, hhead, hmiddle, hsurj⟩
146 refine ⟨?_, ?_, ?_, ?_⟩
147 · intro x y hxy
148 change
149 FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap
150 (H := H) r psi hpsi x =
151 FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap
152 (H := H) r psi hpsi y at hxy
153 exact hinj hxy
154 · intro y
155 change
156 FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap
157 (H := H) r psi y = 0 ↔
158 ∃ x,
159 FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap
160 (H := H) r psi hpsi x = y
161 exact hhead y
162 · intro y
163 change augmentation H y = 0 ↔
164 ∃ x,
165 FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap
166 (H := H) r psi x = y
167 exact hmiddle y
168 · intro z
169 rcases hsurj z with ⟨y, hy⟩
170 refine ⟨y, ?_⟩
171 change augmentation H y = z
172 exact hy
174end
176end CrowellExactSequence