CrowellExactSequence/Discrete/BlanchfieldLyndon.lean
1import CrowellExactSequence.FiniteFamilyExactness
2import FoxDifferential.Discrete.KernelBoundary.Quotient
3import FoxDifferential.Discrete.KernelBoundary.MagnusKernel
4import FoxDifferential.Discrete.FoxCalculus.Coordinates
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/CrowellExactSequence/Discrete/BlanchfieldLyndon.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Discrete Blanchfield--Lyndon public maps
18Blanchfield--Lyndon coordinates. The middle term is identified with relative Fox coordinates,
20-/
22namespace CrowellExactSequence
24noncomputable section
26open FoxDifferential
28namespace FoxCalculus
30variable {H : Type} [Group H]
32/-- The coordinate equivalence for a finite free presentation
33`ψ : FreeGroup (Fin r) →* H`. It identifies the Crowell middle term with explicit
34relative Fox coordinates. -/
36 (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
37 DifferentialModule ψ ≃ₗ[GroupRing H] (Fin r → GroupRing H) :=
39 (H := H) (Fin r) ψ).symm
41/-- The concrete BL tail generators `ψ(x_i) - 1` for a finite free presentation. -/
44 fun i => augmentationGenerator H (ψ (FreeGroup.of i))
46/-- The concrete Blanchfield--Lyndon tail map in relative Fox coordinates. -/
48 (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
52 (freeGroupPresentationAugmentationGenerators (H := H) r ψ)
54/-- Concrete finite-sum form of the BL tail map. -/
57 freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r ψ a =
58 ∑ i : Fin r, a i * augmentationGenerator H (ψ (FreeGroup.of i)) := by
60 simp only [freeGroupPresentationAugmentationGenerators, augmentationGenerator_eq_groupRingBoundary,
61 smul_eq_mul]
63/-- The concrete BL head map: the Crowell head map written in relative Fox coordinates. -/
65 (r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ) :
66 letI := kernelAbelianizationModuleOfSurjective ψ hψ
67 KernelAbelianizationAdd ψ →ₗ[GroupRing H] (Fin r → GroupRing H) := by
68 letI := kernelAbelianizationModuleOfSurjective ψ hψ
69 exact
70 (freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap.comp
73/-- On a kernel element, the concrete BL head map is the relative Fox derivative vector. -/
75 (r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ)
76 (n : ψ.ker) :
77 letI := kernelAbelianizationModuleOfSurjective ψ hψ
78 freeGroupPresentationRelativeDerivativeHeadMap (H := H) r ψ hψ
79 (Additive.ofMul (Abelianization.of n)) =
80 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1 := by
81 letI := kernelAbelianizationModuleOfSurjective ψ hψ
82 change
83 (freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap
85 (Additive.ofMul (Abelianization.of n))) =
86 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
88 change
90 (H := H) (Fin r) ψ (universalDifferential ψ n.1) =
91 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
93 (H := H) (Fin r) ψ n.1
95end FoxCalculus
97open scoped BigOperators
99namespace Morishita2024
101variable {H : Type} [Group H]
103/-- Discrete Crowell exact sequence for a surjective group homomorphism. -/
105 {G : Type} [Group G]
106 (psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
107 letI := kernelAbelianizationModuleOfSurjective psi hpsi
108 Function.Injective
109 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi) ∧
110 Function.Exact
111 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
112 (toGroupRing psi) ∧
113 Function.Exact (toGroupRing psi) (augmentation H) ∧
114 Function.Surjective (augmentation H) := by
115 letI := kernelAbelianizationModuleOfSurjective psi hpsi
116 refine ⟨?_, ?_, exact_toGroupRing_augmentation (H := H) psi hpsi,
117 augmentation_surjective (H := H)⟩
118 · exact FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
119 (H := H) (ψ := psi) hpsi
120 · exact exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing (H := H) psi hpsi
122/-- Discrete Blanchfield--Lyndon exact sequence for a surjective finite free presentation. -/
124 (r : Nat) (psi : MonoidHom (FreeGroup (Fin r)) H) (hpsi : Function.Surjective psi) :
125 letI := kernelAbelianizationModuleOfSurjective psi hpsi
126 Function.Injective
127 (FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi) ∧
128 Function.Exact
129 (FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi)
130 (FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi) ∧
131 Function.Exact
132 (FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi)
133 (augmentation H) ∧
134 Function.Surjective (augmentation H) := by
135 letI := kernelAbelianizationModuleOfSurjective psi hpsi
136 let e : DifferentialModule psi ≃ₗ[GroupRing H] (Fin r → GroupRing H) :=
137 FoxCalculus.freeGroupPresentationMiddleCoordinateEquiv (H := H) r psi
139 FoxCalculus.freeGroupPresentationAugmentationGenerators (H := H) r psi
140 change
141 Function.Injective
142 (e.toLinearMap.comp
143 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)) ∧
144 Function.Exact
145 (e.toLinearMap.comp
146 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi))
147 (blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators) ∧
148 Function.Exact
149 (blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators)
150 (augmentation H) ∧
151 Function.Surjective (augmentation H)
152 have hfox :
153 blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators =
154 (toGroupRing psi).comp e.symm.toLinearMap := by
155 change
156 FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi =
157 (toGroupRing psi).comp
159 (H := H) (Fin r) psi)
161 apply LinearMap.ext
162 intro a
163 rw [FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap_apply]
164 simp only [augmentationGenerator_eq_groupRingBoundary, FoxCalculus.relativeFreeGroupFoxBoundary,
165 LinearMap.coe_mk, AddHom.coe_mk]
166 have htoAug_exact :
167 Function.Exact
168 (e.toLinearMap.comp
169 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi))
170 ((toAugmentationIdeal (H := H) psi).comp e.symm.toLinearMap) := by
171 exact
172 (LinearEquiv.conj_exact_iff_exact
173 (f := kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
174 (g := toAugmentationIdeal (H := H) psi) e).2
176 (H := H) psi hpsi)
177 have hfree_inj :
178 Function.Injective
179 (e.toLinearMap.comp
180 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)) := by
181 intro x y hxy
182 apply FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
183 (H := H) (ψ := psi) hpsi
184 apply e.injective
185 simpa using hxy
186 refine ⟨hfree_inj, ?_, ?_, augmentation_surjective (H := H)⟩
187 · rw [hfox, ← subtype_comp_toAugmentationIdeal (H := H) psi]
188 exact
189 (Function.Injective.comp_exact_iff_exact
190 (R := GroupRing H) ((augmentationIdeal H).subtype_injective)).2
191 htoAug_exact
192 · rw [hfox]
193 intro z
194 constructor
195 · intro hz
196 rcases (exact_toGroupRing_augmentation (H := H) psi hpsi z).1 hz with ⟨x, hx⟩
197 rcases e.symm.surjective x with ⟨y, rfl⟩
198 exact ⟨y, hx⟩
199 · rintro ⟨y, rfl⟩
200 exact augmentation_toGroupRing_eq_zero (H := H) psi (e.symm y)
202end Morishita2024
204end
206end CrowellExactSequence