Sheaf Cohomology API #
Centralizes results about sheaf cohomology Sheaf.H, keeping the underlying Ext
calculations internal so downstream files never need to unfold Sheaf.H directly.
Main results #
subsingleton_sheafH_of_shortExact_middle: middle-term cohomology vanishingsheafH_subsingleton_of_isEmpty: empty-space vanishingsheaf_isZero_of_zero_stalks: zero stalks imply zero sheafsheafH_subsingleton_of_isZero: bundled zero-sheaf vanishingstalk_zero_of_ses_g_iso: stalk vanishing from SES with iso ongstalk_zero_of_shortExact_kernel: stalk vanishing from SES kernelstalk_zero_of_g_is_cokernel_of_stalk_epi: sheaf-level stalk vanishing from a cokernel and stalk-epi hypothesiscokernel_stalk_zero_of_stalk_surj: actual-cokernel specialization of the same stalk vanishing under stalk-surjectivitysheafHSuccMap: successor connecting morphismsheafH_succ_map_exists_preimage_of_subsingleton_middle: successor-map preimage wrappersheafH0EquivSections: sheaf-level wrapper forH^0(F) ≃+ F(⊤)sheafH0EquivSections_natural: sheaf-level naturality of the abovesheafH1CokernelIsoOfSubsingletonMiddle: sheaf-level form of theH¹cokernel identificationsheafH1_cokernel_iso_of_subsingleton_middle_natural: sheaf-level naturality for the sameH¹cokernel identificationsheafHSuccIsoOfSubsingletonMiddle: sheaf-level form of the higher-degree connecting isomorphismsheafH_succ_iso_of_subsingleton_middle_natural: sheaf-level naturality for the same connecting isomorphismsheafH0_surj_of_epi_app_top: sheaf-level surjectivity on top sections gives H^0 surjectivitysheafH_subsingleton_H1_via_surj: sheaf-level H^1 vanishing via H^0-surjectivitysheafH_subsingleton_H1_via_epi_app_top: sheaf-level H^1 vanishing via surjective top sectionssheafH_subsingleton_of_injective: positive-degree cohomology of an injective sheaf is subsingletonsheafH_subsingleton_H1_of_injective_of_epi_app_top: sheaf-level injective-middle-termH¹vanishingsheafH_dimension_shift_of_both: sheaf-level forward dimension shift for short exact sequencessheafH_dimension_shift_of_mono: forward dimension shift for a monomorphismsheafH_dimension_shift_of_injective: forward dimension shift with injective middle termsheafH_dimension_shift_X₃_of_locallySurjective: reverse dimension shift for locally surjective morphisms
Equations
- sheafPreadditive X = { homGroup := fun (P Q : TopCat.Sheaf AddCommGrpCat X) => CategoryTheory.Preadditive.homGroup P Q, add_comp := ⋯, comp_add := ⋯ }
Internal Ext helpers #
The connecting morphism in the covariant long exact sequence as an additive equivalence,
assuming the middle cohomology groups in degrees n and n + 1 vanish.
Equations
- extClassPostcompAddEquivOfSubsingletonMiddle Z hS n h₂n h₂succ = AddEquiv.ofBijective (hS.extClass.postcomp Z ⋯) ⋯
Instances For
Stalks and zero sheaves #
Successor connecting morphism attached to a short exact sequence of sheaves.
Equations
- sheafHSuccMap hS n = AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun (y : CategoryTheory.Sheaf.H S.X₃ n) => CategoryTheory.Abelian.Ext.comp y hS.extClass ⋯) ⋯)
Instances For
If the middle term has subsingleton cohomology in degree n + 1, every
H^(n+1)(S.X₁) class comes from some H^n(S.X₃) class via the successor map.
If a bundled sheaf is zero, then its cohomology is subsingleton in every degree.
In a short exact sequence X₁ → X₂ → X₃, if the stalk map of g at x is an
isomorphism, then the stalk of X₁ at x vanishes.
In a short exact sequence X₁ → X₂ → X₃, if all stalks of X₂ at x vanish, then
all stalks of X₁ at x vanish (by mono-injectivity of f).
If g is a cokernel of f and the stalk map of f at x is epi, then the stalk
of S.X₃ at x vanishes.
Actual-cokernel specialization of
stalk_zero_of_g_is_cokernel_of_stalk_epi: if the stalk map of f at x
is surjective, then the stalk of cokernel f at x vanishes.
H⁰ ≅ Sections #
If F is a sheaf, then H F 0 is equivalent to sections on ⊤.
Equations
Instances For
Naturality of sheafH0EquivSections: composing x with mk₀ f at
degree 0 corresponds to applying f.app(⊤) on sections.
H¹(S.X₁) as the cokernel of top sections for a short exact sequence of sheaves,
assuming H¹(S.X₂) is subsingleton.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If a sheaf morphism is surjective on top sections, then every degree-zero cohomology class of the target lifts along it.
H¹ vanishing via degree-zero surjectivity.
H¹ vanishing criterion from surjective top sections.
Positive-degree cohomology of an injective sheaf is subsingleton.
H¹ vanishing criterion with injective middle term.
Forward dimension shift for a short exact sequence of sheaves.
Forward dimension shift for a monomorphism of sheaves:
if f : F ⟶ G is mono, the cokernel sheaf has subsingleton H^n, and
G has subsingleton H^(n+1), then F has subsingleton H^(n+1).
Forward dimension shifting with injective middle term:
if 0 → S.X₁ → S.X₂ → S.X₃ → 0 is short exact, S.X₂ is injective,
and H^n(S.X₃)=0, then H^(n+1)(S.X₁)=0.
Reverse dimension shift for a locally surjective morphism:
if f : F ⟶ G is locally surjective, H^n(F) is subsingleton, and
H^(n+1)(kernel f) is subsingleton, then H^n(G) is subsingleton.
If X is empty, then the cohomology of every sheaf on X is subsingleton.
Sheaf Cohomology Functor #
The sheaf cohomology functor H^n : Sheaf(X, Ab) ⥤ Ab, defined as the covariant
Ext functor Ext^n(ℤ_X, −) where ℤ_X is the constant sheaf of integers.
Equations
Instances For
Middle-term cohomology vanishing: if f : F ⟶ G is mono and the cohomology of F
and cokernel f are subsingleton in degree n, then so is the cohomology of G.
Naturality of sheafH1CokernelIsoOfSubsingletonMiddle for a morphism between
two short exact sequences of sheaves.
The degree-0 sheaf cohomology functor is naturally isomorphic to taking sections on ⊤.
Equations
- sheafH0NatIsoSections = CategoryTheory.NatIso.ofComponents (fun (F : TopCat.Sheaf AddCommGrpCat X) => (sheafH0EquivSections F).toAddCommGrpIso) ⋯
Instances For
Higher-degree connecting additive equivalence for a short exact sequence of sheaves:
if the middle cohomology groups in degrees n and n + 1 are subsingleton, then the
connecting morphism induces an additive equivalence H^n(S.X₃) ≃+ H^(n+1)(S.X₁).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Higher-degree connecting isomorphism for a short exact sequence of sheaves: if the
middle cohomology groups in degrees n and n + 1 are subsingleton, then the connecting
morphism induces an isomorphism H^n(S.X₃) ≅ H^(n+1)(S.X₁).
Equations
- sheafHSuccIsoOfSubsingletonMiddle hS n h₂n h₂succ = (sheafHExtClassAddEquivOfSubsingletonMiddle hS n h₂n h₂succ).toAddCommGrpIso
Instances For
Naturality of sheafHSuccIsoOfSubsingletonMiddle for a morphism between two
short exact sequences of sheaves.