feat(CategoryTheory): Add exact sequences for Sheaf Cohomology#36218
feat(CategoryTheory): Add exact sequences for Sheaf Cohomology#36218Brian-Nugent wants to merge 33 commits intoleanprover-community:masterfrom
Conversation
Co-authored-by: Adam Topaz <[email protected]>
… Additive instances for constant sheaves
…or better clarity and functionality
…ved clarity and structure
…nce in sheaf cohomology
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
github-actions
bot
added
the
merge-conflict
github-actions
bot
added
large-import
PR summary b301d257a1Import changes exceeding 2%
|
| 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%) |
Import changes for all files
| Files | Import difference |
|---|---|
21 filesMathlib.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 |
Mathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences (new file) |
1753 |
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
+ connectingHom
+ connectingHom_naturality
+ 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
+ longSequence
+ longSequenceFunctor
+ longSequence_equiv₀_exact₃
+ longSequence_exact
+ longSequence_exact₁
+ longSequence_exact₁'
+ longSequence_exact₂
+ longSequence_exact₂'
+ longSequence_exact₃
+ longSequence_exact₃'
+ longSequence_hom
+ uliftZMultiplesHom.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) = (2.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 6897 | 2 | backward.isDefEq |
Current commit 9374a27700
Reference commit b301d257a1
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
|
This PR/issue depends on:
|
…nitions for consistency
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
Brian-Nugent
changed the title
Brian-Nugent
added
t-category-theory
1 participant
In this PR, I add the long exact sequence for sheaf cohomology as well as prove that it is functorial. Since sheaf cohomology is defined in terms of
Ext, this is done using the covariant sequence forExt.