Cohomological boundedness from a finite acyclic open cover

A nonempty list of opens is IntersectionAcyclic when the coefficient sheaf has vanishing positive local cohomology on every nonempty intersection of members of the list. Repeated Mayer--Vietoris then bounds the cohomology of their union by the length of the list.

def CategoryTheory.Sheaf.opensUnion {X : TopCat} : List (TopologicalSpace.Opens ↑X) → TopologicalSpace.Opens ↑X

The union of a finite list of opens.

Equations

• CategoryTheory.Sheaf.opensUnion = List.foldr (fun (x1 x2 : TopologicalSpace.Opens ↑X) => x1 ⊔ x2) ⊥

@[simp]

theorem CategoryTheory.Sheaf.opensUnion_nil {X : TopCat} : opensUnion [] = ⊥

@[simp]

theorem CategoryTheory.Sheaf.opensUnion_cons {X : TopCat} (U : TopologicalSpace.Opens ↑X) (L : List (TopologicalSpace.Opens ↑X)) : opensUnion (U :: L) = U ⊔ opensUnion L

@[simp]

theorem CategoryTheory.Sheaf.inf_opensUnion {X : TopCat} (U : TopologicalSpace.Opens ↑X) (L : List (TopologicalSpace.Opens ↑X)) : U ⊓ opensUnion L = opensUnion (List.map (fun (x : TopologicalSpace.Opens ↑X) => U ⊓ x) L)

inductive CategoryTheory.Sheaf.IntersectionAcyclic {X : TopCat} (F : TopCat.Sheaf AddCommGrpCat X) (hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)) : List (TopologicalSpace.Opens ↑X) → Prop

Positive local cohomology vanishes on every nonempty intersection generated by a list.

For U :: L, besides acyclicity on U and on intersections generated by L, the third field records acyclicity on intersections which also contain U.

• nil {X : TopCat} {F : TopCat.Sheaf AddCommGrpCat X} {hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)} : IntersectionAcyclic F hExt []
• cons {X : TopCat} {F : TopCat.Sheaf AddCommGrpCat X} {hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)} (U : TopologicalSpace.Opens ↑X) (L : List (TopologicalSpace.Opens ↑X)) (head : ∀ (n : ℕ), 0 < n → Subsingleton (CategoryTheory.Sheaf.localHPrime✝ hExt F n U)) (tail : IntersectionAcyclic F hExt L) (intersections : IntersectionAcyclic F hExt (List.map (fun (x : TopologicalSpace.Opens ↑X) => U ⊓ x) L)) : IntersectionAcyclic F hExt (U :: L)

theorem CategoryTheory.Sheaf.HPrime_subsingleton_opensUnion_of_intersectionAcyclic {X : TopCat} (F : TopCat.Sheaf AddCommGrpCat X) [hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)] {L : List (TopologicalSpace.Opens ↑X)} (hL : IntersectionAcyclic F hExt L) (hne : L ≠ []) (n : ℕ) (hn : L.length ≤ n) : Subsingleton (CategoryTheory.Sheaf.localHPrime✝ hExt F n (opensUnion L))

A union of m opens with acyclic nonempty intersections has no cohomology in degrees n ≥ m. This is the finite-cover Mayer--Vietoris bound.