Source: ProCGroups.CrowellExactSequence.Discrete.SequenceMaps
1import ProCGroups.CrowellExactSequence.Basic
2import ProCGroups.FoxDifferential.Discrete.KernelBoundary.Quotient
3import ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusKernel
4import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Coordinates
6/-!
7# Discrete Crowell sequence maps
9This file constructs the maps in the discrete presentation sequence: the middle coordinate
10equivalence, the augmentation-generator tail map, and the relative-derivative head map. It also
11records their formulas on free generators.
12-/
14namespace CrowellExactSequence
16noncomputable section
18open FoxDifferential
20namespace FoxCalculus
22variable {H : Type} [Group H]
24/--
25For a finite free presentation \(\psi:F_r\to H\), the Crowell middle term is identified with
26the explicit module of relative Fox coordinates.
27-/
28def freeGroupPresentationMiddleCoordinateEquiv
29 (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
30 DifferentialModule ψ ≃ₗ[GroupRing H] (Fin r → GroupRing H) :=
32 (H := H) (Fin r) ψ).symm
34/-- The concrete BL tail generators \(\psi(x_i)-1\) for a finite free presentation. -/
35def freeGroupPresentationAugmentationGenerators
36 (r : Nat) (ψ : FreeGroup (Fin r) →* H) : Fin r → GroupRing H :=
37 fun i => augmentationGenerator H (ψ (FreeGroup.of i))
39/-- The concrete Blanchfield--Lyndon tail map in relative Fox coordinates. -/
40def freeGroupPresentationBlanchfieldLyndonTailMap
41 (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
42 (Fin r → GroupRing H) →ₗ[GroupRing H] GroupRing H :=
43 blanchfieldLyndonFiniteFamilyMap
44 (R := GroupRing H)
45 (freeGroupPresentationAugmentationGenerators (H := H) r ψ)
47/--
48The discrete Blanchfield--Lyndon tail map is evaluated on the canonical generators and then
49extended linearly to the coordinate module.
50-/
51theorem freeGroupPresentationBlanchfieldLyndonTailMap_apply
52 (r : Nat) (ψ : FreeGroup (Fin r) →* H) (a : Fin r → GroupRing H) :
53 freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r ψ a =
54 ∑ i : Fin r, a i * augmentationGenerator H (ψ (FreeGroup.of i)) := by
55 rw [freeGroupPresentationBlanchfieldLyndonTailMap, blanchfieldLyndonFiniteFamilyMap_apply]
56 simp only [freeGroupPresentationAugmentationGenerators,
57 augmentationGenerator_eq_groupRingBoundary, smul_eq_mul]
59/-- The concrete BL head map: the Crowell head map written in relative Fox coordinates. -/
60def freeGroupPresentationRelativeDerivativeHeadMap
61 (r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ) :
62 letI := kernelAbelianizationModuleOfSurjective ψ hψ
63 KernelAbelianizationAdd ψ →ₗ[GroupRing H] (Fin r → GroupRing H) := by
64 letI := kernelAbelianizationModuleOfSurjective ψ hψ
65 exact
66 (freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap.comp
67 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
69/-- On a kernel element, the concrete BL head map is the relative Fox derivative vector. -/
70theorem freeGroupPresentationRelativeDerivativeHeadMap_of
71 (r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ)
72 (n : ψ.ker) :
73 letI := kernelAbelianizationModuleOfSurjective ψ hψ
74 freeGroupPresentationRelativeDerivativeHeadMap (H := H) r ψ hψ
75 (Additive.ofMul (Abelianization.of n)) =
76 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1 := by
77 letI := kernelAbelianizationModuleOfSurjective ψ hψ
78 change
79 (freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap
80 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
81 (Additive.ofMul (Abelianization.of n))) =
82 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
83 rw [kernelAbelianizationBoundaryLinearOfSurjective_of]
84 change
86 (H := H) (Fin r) ψ (universalDifferential ψ n.1) =
87 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
89 (H := H) (Fin r) ψ n.1
91end FoxCalculus
93end
95end CrowellExactSequence