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,14 @@ instance AddGrpCat.forget_isCorepresentable :
 instance AddCommGrpCat.forget_isCorepresentable :
     (forget AddCommGrpCat.{u}).IsCorepresentable :=
   Functor.IsCorepresentable.mk' AddCommGrpCat.coyonedaObjIsoForget
+
+theorem uliftZMultiplesHom.map_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` -/
+@[simps!]
+def AddCommGrpCat.uliftZMultiplesAddEquiv (G : AddCommGrpCat) : (of (ULift ℤ) ⟶ G) ≃+ G :=
+  AddEquiv.trans (@AddCommGrpCat.homAddEquiv (AddCommGrpCat.of (ULift ℤ)) G)
+    (AddEquiv.mk' (uliftZMultiplesHom G) (uliftZMultiplesHom.map_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,8 +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.EnoughProjectives
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
 public import Mathlib.Algebra.Category.Grp.Zero
+public import Mathlib.CategoryTheory.Adjunction.Additive
 
 /-!
 # Sheaf cohomology
@@ -108,6 +109,73 @@ abbrev H' (F : Sheaf J AddCommGrpCat.{v}) (n : ℕ) (X : C) :
 
 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 (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.obj.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₀_naturality (x : H F 0) :
+    f.hom.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_naturality (x : F.obj.obj (op T)) :
+    H.map f 0 ((H.equiv₀ F hT).symm x) = (H.equiv₀ G hT).symm (f.hom.app (op T) x) := by
+  apply (H.equiv₀ G hT).injective
+  simp [← H.equiv₀_naturality]
+
+lemma H.map_apply {n : ℕ} (x : H F n) :
+    H.map f n x = x.comp (Ext.mk₀ f) (add_zero n) := rfl
+
+@[simp]
+lemma H.map_id_apply {n : ℕ} (x : H F n) : H.map (𝟙 F) n x = x := by
+  simp [H.map_apply]
+
+lemma H.map_comp_apply {n : ℕ} {G' : Sheaf J AddCommGrpCat.{w}} (g : G ⟶ G') (x : H F n) :
+    H.map (f ≫ g) n x = H.map g n (H.map f n x) := by
+  simp [H.map_apply]
+
+attribute [local simp] H.map_comp_apply in
+variable (J) in
+/-- `H` as a functor. -/
+@[simps]
+noncomputable def functorH (n : ℕ) : Sheaf J AddCommGrpCat.{w} ⥤ AddCommGrpCat.{w'} where
+  obj F := .of (H F n)
+  map f := AddCommGrpCat.ofHom (H.map f n)
+
+set_option backward.isDefEq.respectTransparency false in
+instance (n : ℕ) : (functorH J n).Additive where
+  map_add {_ _ f g} := by ext; simp [H.map_apply, Ext.mk₀_add];
+
+end
+
 end Sheaf
 
 end CategoryTheory