Source: ProCGroups.CrowellExactSequence.Discrete.Exactness
1import ProCGroups.CrowellExactSequence.Discrete.SequenceMaps
3/-!
4# Discrete Crowell exactness
6Surjectivity and the kernel/image identities for the relative Fox derivative assemble into the
7four-term discrete Crowell sequence. The free-group presentation theorem specializes this
8criterion to the Blanchfield--Lyndon exact sequence.
9-/
11namespace CrowellExactSequence
13noncomputable section
15open FoxDifferential
17open scoped BigOperators
19namespace Morishita2024
21variable {H : Type} [Group H]
23/-- Discrete Crowell exact sequence for a surjective group homomorphism. -/
24theorem crowellExactSequence_of_surjective
25 {G : Type} [Group G]
26 (psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
27 letI := kernelAbelianizationModuleOfSurjective psi hpsi
28 Function.Injective
29 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi) ∧
30 Function.Exact
31 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
32 (toGroupRing psi) ∧
33 Function.Exact (toGroupRing psi) (augmentation H) ∧
34 Function.Surjective (augmentation H) := by
35 letI := kernelAbelianizationModuleOfSurjective psi hpsi
36 refine ⟨?_, ?_, exact_toGroupRing_augmentation (H := H) psi hpsi,
37 augmentation_surjective (H := H)⟩
38 · exact FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
39 (H := H) (ψ := psi) hpsi
40 · exact exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing (H := H) psi hpsi
42/-- The discrete Blanchfield--Lyndon exact sequence for a surjective finite free presentation. -/
43theorem freeGroupPresentation_blanchfieldLyndonExactSequence
44 (r : Nat) (psi : MonoidHom (FreeGroup (Fin r)) H) (hpsi : Function.Surjective psi) :
45 letI := kernelAbelianizationModuleOfSurjective psi hpsi
46 Function.Injective
47 (FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi) ∧
48 Function.Exact
49 (FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi)
50 (FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi) ∧
51 Function.Exact
52 (FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi)
53 (augmentation H) ∧
54 Function.Surjective (augmentation H) := by
55 letI := kernelAbelianizationModuleOfSurjective psi hpsi
56 let e : DifferentialModule psi ≃ₗ[GroupRing H] (Fin r → GroupRing H) :=
57 FoxCalculus.freeGroupPresentationMiddleCoordinateEquiv (H := H) r psi
58 let generators : Fin r → GroupRing H :=
59 FoxCalculus.freeGroupPresentationAugmentationGenerators (H := H) r psi
60 change
61 Function.Injective
62 (e.toLinearMap.comp
63 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)) ∧
64 Function.Exact
65 (e.toLinearMap.comp
66 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi))
67 (blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators) ∧
68 Function.Exact
69 (blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators)
70 (augmentation H) ∧
71 Function.Surjective (augmentation H)
72 have hfox :
73 blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators =
74 (toGroupRing psi).comp e.symm.toLinearMap := by
75 change
76 FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi =
77 (toGroupRing psi).comp
79 (H := H) (Fin r) psi)
81 apply LinearMap.ext
82 intro a
83 rw [FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap_apply]
84 simp only [augmentationGenerator_eq_groupRingBoundary, FoxCalculus.relativeFreeGroupFoxBoundary,
85 LinearMap.coe_mk, AddHom.coe_mk]
86 have htoAug_exact :
87 Function.Exact
88 (e.toLinearMap.comp
89 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi))
90 ((toAugmentationIdeal (H := H) psi).comp e.symm.toLinearMap) := by
91 exact
92 (LinearEquiv.conj_exact_iff_exact
93 (f := kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
94 (g := toAugmentationIdeal (H := H) psi) e).2
95 (exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
96 (H := H) psi hpsi)
97 have hfree_inj :
98 Function.Injective
99 (e.toLinearMap.comp
100 (kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)) := by
101 intro x y hxy
102 apply FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
103 (H := H) (ψ := psi) hpsi
104 exact e.injective hxy
105 refine ⟨hfree_inj, ?_, ?_, augmentation_surjective (H := H)⟩
106 · rw [hfox, ← subtype_comp_toAugmentationIdeal (H := H) psi]
107 exact
108 (Function.Injective.comp_exact_iff_exact
109 (R := GroupRing H) ((augmentationIdeal H).subtype_injective)).2
110 htoAug_exact
111 · rw [hfox]
112 intro z
113 constructor
114 · intro hz
115 rcases (exact_toGroupRing_augmentation (H := H) psi hpsi z).1 hz with ⟨x, hx⟩
116 rcases e.symm.surjective x with ⟨y, rfl⟩
117 exact ⟨y, hx⟩
118 · rintro ⟨y, rfl⟩
119 exact augmentation_toGroupRing_eq_zero (H := H) psi (e.symm y)
121end Morishita2024
123end
125end CrowellExactSequence