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/Abelian.lean

@@ -6,9 +6,8 @@ Authors: Adam Topaz, Jujian Zhang
 module
 
 public import Mathlib.CategoryTheory.Abelian.FunctorCategory
-public import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 public import Mathlib.CategoryTheory.Abelian.Transfer
-public import Mathlib.CategoryTheory.Sites.Limits
+public import Mathlib.CategoryTheory.Sites.ConstantSheaf
 
 /-!
 # Category of sheaves is abelian
@@ -46,6 +45,11 @@ attribute [local instance] preservesBinaryBiproducts_of_preservesBinaryProducts
 instance presheafToSheaf_additive : (presheafToSheaf J D).Additive :=
   (presheafToSheaf J D).additive_of_preservesBinaryBiproducts
 
+instance : (Functor.const Cᵒᵖ : D ⥤ Cᵒᵖ ⥤ D).Additive where
+
+instance : (constantSheaf J D).Additive :=
+  inferInstanceAs (Functor.const _ ⋙ presheafToSheaf _ _).Additive
+
 end Abelian
 
 end CategoryTheory

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,62 @@ noncomputable abbrev cohomologyPresheaf (F : Sheaf J AddCommGrpCat.{v}) (n : ℕ
 
 end
 
+section
+
+variable [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
+
+instance (F : Sheaf J AddCommGrpCat.{w}) {n : ℕ} [Injective F] : Subsingleton (H F (n + 1)) :=
+  subsingleton_of_forall_eq 0 fun x ↦ (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 sheaf cohomology. -/
+noncomputable abbrev 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 _ hS n₀ n₁ h
+
+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 ≃+ F.val.obj (op T) :=
+    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) :
+    f.val.app (op T) (H.equiv₀ F hT x) = H.equiv₀ G hT (H.map f 0 x) := by
+  simp only [equiv₀, AddEquiv.trans_apply]
+  erw[addEquiv₀_comp f x]
+  rfl
+
+theorem H.equiv₀_symm_comp (x : F.val.obj (op T)) :
+    H.map f 0 ((H.equiv₀ F hT).symm x) = (H.equiv₀ G hT).symm (f.val.app (op T) x) := by
+  apply (H.equiv₀ G hT).injective
+  simp [← H.equiv₀_comp]
+
+end
+
 end Sheaf
 
 end CategoryTheory