Cohomology.lean

1 import Mathlib.GroupTheory.QuotientGroup.Basic
2 import Mathlib.Tactic.Abel
3 
4 set_option autoImplicit false
5 
6 /-!
7 # The additive obstruction sector
8 
9 C¹ --δ₁--> C² --δ₂--> C³ with δ₂δ₁ = 0.
10 No assertion is made that arbitrary categorical square defects automatically
11 form such a complex. An application must supply and verify this structure.
12 -/
13 universe u v w z
14 namespace KomorebiSpace
15 
16 structure ObstructionComplex (A : Type u) (B : Type v) (C : Type w)
17     [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] where
18   d₁ : A →+ B
19   d₂ : B →+ C
20   square_zero : ∀ a, d₂ (d₁ a) = 0
21 
22 namespace ObstructionComplex
23 variable {A : Type u} {B : Type v} {C : Type w}
24 variable [AddCommGroup A] [AddCommGroup B] [AddCommGroup C]
25 
26 abbrev Cycles (K : ObstructionComplex A B C) := K.d₂.ker
27 
28 def boundaryMap (K : ObstructionComplex A B C) : A →+ K.Cycles where
29   toFun := fun a => ⟨K.d₁ a, K.square_zero a⟩
30   map_zero' := by apply Subtype.ext; exact map_zero K.d₁
31   map_add' := by intro a b; apply Subtype.ext; exact map_add K.d₁ a b
32 
33 abbrev H2 (K : ObstructionComplex A B C) := K.Cycles ⧸ K.boundaryMap.range
34 
35 def obstructionClass (K : ObstructionComplex A B C) (ω : K.Cycles) : K.H2 :=
36   (ω : K.Cycles ⧸ K.boundaryMap.range)
37 
38 theorem class_zero_iff (K : ObstructionComplex A B C) (ω : K.Cycles) :
39     K.obstructionClass ω = 0 ↔ ∃ a, K.d₁ a = ω.val := by
40   change (ω : K.Cycles ⧸ K.boundaryMap.range) = 0 ↔ _
41   rw [QuotientAddGroup.eq_zero_iff]
42   constructor
43   · rintro ⟨a, ha⟩
44     exact ⟨a, congrArg Subtype.val ha⟩
45   · rintro ⟨a, ha⟩
46     exact ⟨a, Subtype.ext ha⟩
47 
48 /-- This is standard cohomological flattening, not a general descent theorem. -/
49 theorem flatten_iff (K : ObstructionComplex A B C) (ω : K.Cycles) :
50     K.obstructionClass ω = 0 ↔ ∃ a, ω.val - K.d₁ a = 0 := by
51   rw [K.class_zero_iff]
52   constructor
53   · rintro ⟨a, ha⟩; exact ⟨a, sub_eq_zero.mpr ha.symm⟩
54   · rintro ⟨a, ha⟩; exact ⟨a, (sub_eq_zero.mp ha).symm⟩
55 
56 def correct (K : ObstructionComplex A B C) (ω : K.Cycles) (a : A) : K.Cycles :=
57   ⟨ω.val - K.d₁ a, by
58     change K.d₂ (ω.val - K.d₁ a) = 0
59     rw [map_sub, K.square_zero, show K.d₂ ω.val = 0 from ω.property, sub_self]⟩
60 
61 /-- Gauge correction does not change the obstruction class. -/
62 theorem correction_invariant (K : ObstructionComplex A B C) (ω : K.Cycles) (a : A) :
63     K.obstructionClass (K.correct ω a) = K.obstructionClass ω := by
64   have hc : K.correct ω a = ω - K.boundaryMap a := rfl
65   have hz : (K.boundaryMap a : K.Cycles ⧸ K.boundaryMap.range) = 0 :=
66     (QuotientAddGroup.eq_zero_iff _).2 ⟨a, rfl⟩
67   change (K.correct ω a : K.Cycles ⧸ K.boundaryMap.range) = _
68   rw [hc, QuotientAddGroup.mk_sub, hz, sub_zero]
69   rfl
70 
71 /-- A globally given primary coboundary never yields a nonzero H² class. -/
72 theorem primary_defect_class_zero (K : ObstructionComplex A B C) (a : A) :
73     K.obstructionClass (K.boundaryMap a) = 0 :=
74   (K.class_zero_iff _).2 ⟨a, rfl⟩
75 
76 theorem obstruction_certificate (K : ObstructionComplex A B C)
77     {D : Type z} [AddCommGroup D] (L : B →+ D)
78     (hL : ∀ a, L (K.d₁ a) = 0) (ω : K.Cycles)
79     (hw : L ω.val ≠ 0) : K.obstructionClass ω ≠ 0 := by
80   intro h
81   rcases (K.class_zero_iff ω).1 h with ⟨a, ha⟩
82   apply hw
83   rw [← ha]
84   exact hL a
85 end ObstructionComplex
86 
87 namespace Differential
88 variable {A : Type u} [AddCommGroup A]
89 
90 /-- Anticommuting differentials use the unsigned total differential d+e. -/
91 theorem anticommuting_sum_square_zero (d e : A →+ A)
92     (hd : ∀ x, d (d x) = 0) (he : ∀ x, e (e x) = 0)
93     (hde : ∀ x, d (e x) + e (d x) = 0) (x : A) :
94     (d + e) ((d + e) x) = 0 := by
95   change d (d x + e x) + e (d x + e x) = 0
96   rw [map_add, map_add, hd, he]
97   simpa only [zero_add, add_zero] using hde x
98 end Differential
99 end KomorebiSpace

Back to source controls