feat(SheafCohomology): add API for Sheaf Cohomology

[Brian-Nugent]

Defines the long exact sequence on cohomology associated to a short exact sequence of sheaves H.longSequence. Also defines H.equiv₀, the additive equivalence between H F 0 and ((sheafSections J AddCommGrpCat).obj (op T)).obj F when the category has a terminal object T.

---

[github-actions]

PR summary b301d257a1

Import changes exceeding 2%

%	File
+30.22%	Mathlib.Algebra.Category.Grp.ForgetCorepresentable
+31.97%	Mathlib.CategoryTheory.Sites.Abelian

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Sites.Abelian	804	1061	+257 (+31.97%)
Mathlib.Algebra.Category.Grp.ForgetCorepresentable	503	655	+152 (+30.22%)
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic	1751	1752	+1 (+0.06%)

Import changes for all files

Files	Import difference
21 files Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris Mathlib.Condensed.AB Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Monoidal Mathlib.Condensed.Light.Small Mathlib.Condensed.Solid Mathlib.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Flasque	1
Mathlib.Condensed.Limits Mathlib.Condensed.Module	22
Mathlib.Topology.Sheaves.MayerVietoris	65
Mathlib.CategoryTheory.Sites.MayerVietorisSquare	146
Mathlib.Algebra.Category.Grp.ForgetCorepresentable	152
Mathlib.CategoryTheory.Sites.Abelian	257

---

Declarations diff

+ AddCommGrpCat.uliftZMultiplesAddEquiv
+ H.addEquiv₀_comp
+ H.equiv₀
+ H.equiv₀_naturality
+ H.equiv₀_symm_naturality
+ H.map
+ H.map_apply
+ H.map_comp_apply
+ H.map_id_apply
+ functorH
+ instance (F : Sheaf J AddCommGrpCat.{w}) {n : ℕ} [Injective F] : Subsingleton (H F (n + 1))
+ instance (n : ℕ) : (functorH J n).Additive
+ instance : (Functor.const Cᵒᵖ : D ⥤ Cᵒᵖ ⥤ D).Additive
+ instance : (constantSheaf J D).Additive
+ uliftZMultiplesHom.map_add

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
6896	1	backward.isDefEq

Current commit 868205ec99
Reference commit b301d257a1

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joneugster]

you can now comment on the PR to add/remove topic labels in cases where the script does not add them correctly:

t-category-theory

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[adamtopaz]

Sorry to keep you waiting. This is getting close now!

[Brian-Nugent]

Should I tag this with @[simp]? I'm still getting used to when this is useful.

[joelriou]

I would say it is unclear in which direction the lemma would be the most useful, so that not putting a simp attribute seems fine to me.

[joelriou]

Suggested change

	lemma H.addEquiv₀_comp (x : H F 0) : Ext.addEquiv₀ (H.map f 0 x) = Ext.addEquiv₀ x ≫ f := by
	@[reassoc]
	lemma H.addEquiv₀_map (x : H F 0) : Ext.addEquiv₀ (H.map f 0 x) = Ext.addEquiv₀ x ≫ f := by