feat(SheafCohomology): add API for Sheaf Cohomology

Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.Grp.Basic
 public import Mathlib.CategoryTheory.Yoneda
+public import Mathlib.Algebra.Category.Grp.Preadditive
 
 /-!
 # The forget functor is corepresentable
@@ -79,3 +80,13 @@ instance AddGrpCat.forget_isCorepresentable :
 instance AddCommGrpCat.forget_isCorepresentable :
     (forget AddCommGrpCat.{u}).IsCorepresentable :=
   Functor.IsCorepresentable.mk' AddCommGrpCat.coyonedaObjIsoForget
+
+theorem uliftZMultiplesHom.add (G : Type u) [AddCommGroup G] (x y : G) :
+    (uliftZMultiplesHom G) (x + y) = ((uliftZMultiplesHom G) x) + ((uliftZMultiplesHom G) y) := by
+  ext
+  simp_all only [uliftZMultiplesHom_apply_apply, smul_add, AddMonoidHom.add_apply]
+
+/-- The additive equivalence `(ℤ ⟶ G) ≃+ G` -/
+def AddCommGrpCat.uliftZMultiplesAddEquiv (G : AddCommGrpCat) : (of (ULift ℤ) ⟶ G) ≃+ ↑G :=
+  AddEquiv.trans (@AddCommGrpCat.homAddEquiv (AddCommGrpCat.of (ULift ℤ)) G)
+    (AddEquiv.mk' (uliftZMultiplesHom G) (uliftZMultiplesHom.add G)).symm

Mathlib/CategoryTheory/Sites/SheafCohomology/Basic.lean

@@ -10,6 +10,9 @@ public import Mathlib.Algebra.Category.Grp.Adjunctions
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
 public import Mathlib.CategoryTheory.Sites.Abelian
 public import Mathlib.CategoryTheory.Sites.ConstantSheaf
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
+public import Mathlib.Algebra.Category.Grp.Zero
+public import Mathlib.CategoryTheory.Adjunction.Additive
 
 /-!
 # Sheaf cohomology
@@ -85,6 +88,68 @@ noncomputable abbrev cohomologyPresheaf (F : Sheaf J AddCommGrpCat.{v}) (n : ℕ
 
 end
 
+section
+
+variable [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
+
+theorem H.eq_zero_of_injective (F : Sheaf J AddCommGrpCat.{w}) (n : ℕ) (x : H F (n + 1))
+    [Injective F] : x = 0 :=
+  Ext.eq_zero_of_injective x
+
+variable {S : ShortComplex (Sheaf J AddCommGrpCat.{w})} (hS : S.ShortExact) (n₀ n₁ : ℕ)
+    (h : n₀ + 1 = n₁)
+
+/-- The long exact sequence on cohomology obtained from a short exact sequence of sheaves:
+If `S` is a short exact sequence of abelian sheaves, then this is the sequence
+`H S.X₁ n₀ → H S.X₂ n₀ → H S.X₃ n₀ → H S.X₁ n₁ → H S.X₂ n₁ → H S.X₃ n₁` when `n₀ + 1 = n₁` -/
+noncomputable def H.longSequence (h : n₀ + 1 = n₁ := by lia) : ComposableArrows AddCommGrpCat 5 :=
+  Ext.covariantSequence ((constantSheaf J AddCommGrpCat.{w}).obj (AddCommGrpCat.of.{w} (ULift ℤ)))
+    hS n₀ n₁ h
+
+theorem H.longSequence.exact (h : n₀ + 1 = n₁ := by lia) : (H.longSequence hS n₀ n₁ h).Exact :=
+  Ext.covariantSequence_exact ((constantSheaf J AddCommGrpCat).obj (AddCommGrpCat.of (ULift ℤ)))
+    hS n₀ n₁ h
+
+instance : (Functor.const Cᵒᵖ : AddCommGrpCat ⥤ Cᵒᵖ ⥤ AddCommGrpCat).Additive where
+
+instance : (constantSheaf J AddCommGrpCat).Additive :=
+  inferInstanceAs (Functor.const _ ⋙ presheafToSheaf _ _).Additive
+
+variable (F : Sheaf J AddCommGrpCat.{w}) {T : C} (hT : Limits.IsTerminal T)
+
+open AddCommGrpCat Opposite
+
+/-- The additive equivalence between `H F 0` and the evaluation of `F` at the terminal object -/
+noncomputable def H.equiv₀ : H F 0 ≃+ ((sheafSections J AddCommGrpCat).obj (op T)).obj F :=
+    AddEquiv.trans Ext.addEquiv₀ (
+      AddEquiv.trans ((constantSheafAdj J AddCommGrpCat hT).homAddEquiv _ F)
+        (uliftZMultiplesAddEquiv _))
+
+variable {F G : Sheaf J AddCommGrpCat.{w}} (f : F ⟶ G)
+
+/-- Given a morphism of sheaves `f : F ⟶ G`, `H.map f n` is the induced additive map on cohomology
+    groups `H F n →+ H G n` -/
+noncomputable def H.map (n : ℕ) : H F n →+ H G n :=
+  ((Ext.mk₀ f).postcomp ((constantSheaf J AddCommGrpCat).obj (of (ULift ℤ))) (add_zero n))
+
+lemma H.addEquiv₀_comp (x : H F 0) : Ext.addEquiv₀ (H.map f 0 x) = Ext.addEquiv₀ x ≫ f := by
+  delta Ext.addEquiv₀ H.map
+  apply (Ext.mk₀_bijective _ G).injective
+  simp only [AddEquiv.coe_mk, Ext.mk₀_homEquiv₀_apply, Ext.mk₀_homEquiv₀_apply, ← Ext.mk₀_comp_mk₀]
+  rfl
+
+/-- `H.Equiv₀` is natural -/
+theorem H.Equiv₀_comp (x : H F 0) :
+    ((sheafSections J AddCommGrpCat).obj (op T)).map f (H.equiv₀ F hT x) =
+    H.equiv₀ G hT (H.map f 0 x) := by
+  delta equiv₀
+  simp only [Functor.flip_obj_obj, sheafToPresheaf_obj, Functor.flip_obj_map, sheafToPresheaf_map,
+    AddEquiv.trans_apply]
+  conv => rhs; right; right; equals Ext.addEquiv₀ x ≫ f => exact addEquiv₀_comp f x
+  rfl
+
+end
+
 end Sheaf
 
 end CategoryTheory