Cohomology.lean

1 import Mathlib.LinearAlgebra.Quotient.Basic
2 import Mathlib.LinearAlgebra.Pi
3 import Mathlib.Algebra.DirectSum.Module
4 import Mathlib.Tactic
5 
6 /-!
7 Paper X, Block 04. Actual three-term cohomology ker(d_out)/im(d_in),
8 with functorial maps induced by cochain maps. No decomposition is assumed.
9 A three-term window at any degree is enough to compute that degree's cohomology.
10 -/
11 set_option autoImplicit false
12 namespace PaperX.Cohomology
13 
14 universe u v
15 
16 /-- Three consecutive terms of a cochain complex, including d_out d_in = 0. -/
17 structure Triple (R : Type u) [CommRing R] where
18   X₀ : Type v
19   X₁ : Type v
20   X₂ : Type v
21   [add₀ : AddCommGroup X₀]
22   [add₁ : AddCommGroup X₁]
23   [add₂ : AddCommGroup X₂]
24   [mod₀ : Module R X₀]
25   [mod₁ : Module R X₁]
26   [mod₂ : Module R X₂]
27   d₀ : X₀ →ₗ[R] X₁
28   d₁ : X₁ →ₗ[R] X₂
29   square : d₁.comp d₀ = 0
30 
31 attribute [instance] Triple.add₀ Triple.add₁ Triple.add₂ Triple.mod₀ Triple.mod₁ Triple.mod₂
32 
33 variable {R : Type u} [CommRing R]
34 
35 /-- A genuine cochain map on the three-term window. -/
36 structure ChainMap (C D : Triple.{u,v} R) where
37   left : C.X₀ →ₗ[R] D.X₀
38   middle : C.X₁ →ₗ[R] D.X₁
39   right : C.X₂ →ₗ[R] D.X₂
40   comm₀ : D.d₀.comp left = middle.comp C.d₀
41   comm₁ : D.d₁.comp middle = right.comp C.d₁
42 
43 variable (C : Triple.{u,v} R)
44 
45 abbrev Cycles := LinearMap.ker C.d₁
46 
47 def incomingCycles : C.X₀ →ₗ[R] Cycles C :=
48   C.d₀.codRestrict (Cycles C) (fun x => by
49     change C.d₁ (C.d₀ x) = 0
50     exact LinearMap.congr_fun C.square x)
51 
52 def boundaries : Submodule R (Cycles C) := LinearMap.range (incomingCycles C)
53 
54 /-- Cohomology is an actual quotient module, not a dimension or named placeholder. -/
55 abbrev H := (Cycles C) ⧸ boundaries C
56 
57 def classOf : Cycles C →ₗ[R] H C := (boundaries C).mkQ
58 
59 theorem classOf_surjective : Function.Surjective (classOf C) :=
60   Submodule.mkQ_surjective _
61 
62 theorem classOf_eq_zero_iff (x : Cycles C) :
63     classOf C x = 0 ↔ ∃ y : C.X₀, C.d₀ y = x.1 := by
64   change (Submodule.Quotient.mk x : H C) = 0 ↔ _
65   rw [Submodule.Quotient.mk_eq_zero]
66   change (∃ y, incomingCycles C y = x) ↔ _
67   constructor
68   · rintro ⟨y, h⟩
69     exact ⟨y, congrArg Subtype.val h⟩
70   · rintro ⟨y, h⟩
71     exact ⟨y, Subtype.ext h⟩
72 
73 variable {C} {D E : Triple.{u,v} R}
74 
75 def cyclesMap (f : ChainMap C D) : Cycles C →ₗ[R] Cycles D :=
76   (f.middle.comp (Cycles C).subtype).codRestrict (Cycles D) (fun x => by
77     change D.d₁ (f.middle x.1) = 0
78     calc
79       _ = f.right (C.d₁ x.1) := LinearMap.congr_fun f.comm₁ x.1
80       _ = 0 := by rw [x.property, map_zero])
81 
82 @[simp] theorem cyclesMap_val (f : ChainMap C D) (x : Cycles C) :
83     (cyclesMap f x).val = f.middle x.val := rfl
84 
85 theorem cyclesMap_incoming (f : ChainMap C D) (x : C.X₀) :
86     cyclesMap f (incomingCycles C x) = incomingCycles D (f.left x) := by
87   apply Subtype.ext
88   exact (LinearMap.congr_fun f.comm₀ x).symm
89 
90 def hmap (f : ChainMap C D) : H C →ₗ[R] H D :=
91   (boundaries C).liftQ ((classOf D).comp (cyclesMap f)) (by
92     rintro x ⟨y, rfl⟩
93     change classOf D (cyclesMap f (incomingCycles C y)) = 0
94     rw [cyclesMap_incoming, classOf_eq_zero_iff]
95     exact ⟨f.left y, rfl⟩)
96 
97 @[simp] theorem hmap_classOf (f : ChainMap C D) (x : Cycles C) :
98     hmap f (classOf C x) = classOf D (cyclesMap f x) := rfl
99 
100 /-- Equality of induced maps needs equality on cocycles, not arbitrary choices of representatives. -/
101 theorem hmap_ext (f g : ChainMap C D)
102     (h : ∀ x : Cycles C, f.middle x.1 = g.middle x.1) : hmap f = hmap g := by
103   apply LinearMap.ext
104   intro z
105   obtain ⟨x, rfl⟩ := classOf_surjective C z
106   rw [hmap_classOf, hmap_classOf]
107   congr 1
108   exact Subtype.ext (h x)
109 
110 def identityMap (C : Triple.{u,v} R) : ChainMap C C where
111   left := LinearMap.id
112   middle := LinearMap.id
113   right := LinearMap.id
114   comm₀ := by simp
115   comm₁ := by simp
116 
117 def compose (g : ChainMap D E) (f : ChainMap C D) : ChainMap C E where
118   left := g.left.comp f.left
119   middle := g.middle.comp f.middle
120   right := g.right.comp f.right
121   comm₀ := by rw [← LinearMap.comp_assoc, g.comm₀, LinearMap.comp_assoc,
122     f.comm₀, ← LinearMap.comp_assoc]
123   comm₁ := by rw [← LinearMap.comp_assoc, g.comm₁, LinearMap.comp_assoc,
124     f.comm₁, ← LinearMap.comp_assoc]
125 
126 @[simp] theorem hmap_identity : hmap (identityMap C) = LinearMap.id := by
127   apply LinearMap.ext
128   intro z
129   obtain ⟨x, rfl⟩ := classOf_surjective C z
130   rfl
131 
132 @[simp] theorem hmap_compose (g : ChainMap D E) (f : ChainMap C D) :
133     hmap (compose g f) = (hmap g).comp (hmap f) := by
134   apply LinearMap.ext
135   intro z
136   obtain ⟨x, rfl⟩ := classOf_surjective C z
137   rfl
138 
139 end PaperX.Cohomology

Back to source controls