feat(SheafCohomology): add API for Sheaf Cohomology#34742
feat(SheafCohomology): add API for Sheaf Cohomology#34742Brian-Nugent wants to merge 19 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
new-contributor
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%) |
| Mathlib.CategoryTheory.Sites.SheafCohomology.Basic | 1751 | 1752 | +1 (+0.06%) |
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 |
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
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).
|
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 |
Co-authored-by: Adam Topaz <[email protected]>
dagurtomas
added
the
awaiting-author
… Additive instances for constant sheaves
Brian-Nugent
removed
the
awaiting-author
…or better clarity and functionality
joelriou
added
the
awaiting-author
Brian-Nugent
removed
the
awaiting-author
joelriou
added
the
awaiting-author
Brian-Nugent
removed
the
awaiting-author
…ved clarity and structure
joelriou
added
the
awaiting-author
Brian-Nugent
removed
the
awaiting-author
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
adamtopaz
left a comment
adamtopaz
left a comment
There was a problem hiding this comment.
Sorry to keep you waiting. This is getting close now!
| 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 := |
There was a problem hiding this comment.
This definition needs a few API lemmas. I don't know whether @[simps!] adds useful lemmas in this case (you can check with @[simps!?]).
There was a problem hiding this comment.
It looks like that added two and they look pretty useful to me. Thank you for this tip, I didn't know I could do this!
| (h : n₀ + 1 = n₁) | ||
|
|
||
| /-- The long exact sequence on sheaf cohomology. -/ | ||
| noncomputable abbrev H.longSequence (h : n₀ + 1 = n₁ := by lia) : |
There was a problem hiding this comment.
I'm not sure this should be an abbrev. Could you say why you made it so?
There was a problem hiding this comment.
I initially had it as a def then someone suggested removing it entirely and just working with Ext.covariantSequence directly, but that would cause us to have to write ((constantSheaf J AddCommGrpCat.{w}).obj (AddCommGrpCat.of.{w} (ULift ℤ))) every time so I figured making it an abbrev was a good compromise.
There was a problem hiding this comment.
I think the way I do it in #36218 is better anyway so I can just delete it here.
adamtopaz
added
the
awaiting-author
| 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 |
There was a problem hiding this comment.
Should I tag this with @[simp]? I'm still getting used to when this is useful.
Brian-Nugent
removed
the
awaiting-author
Brian-Nugent
removed
the
new-contributor
6 participants
Defines the long exact sequence on cohomology associated to a short exact sequence of sheaves
H.longSequence. Also definesH.equiv₀, the additive equivalence betweenH F 0and((sheafSections J AddCommGrpCat).obj (op T)).obj Fwhen the category has a terminal objectT.