Module

DerivedLocalCohomologyMayerVietoris.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyMayerVietoris

1 declaration indexed from sourceView source ↗

Module documentation

Mayer--Vietoris vanishing for derived local cohomology

The exact filtered-colimit window in positions two, three, and four of the ideal-quotient derived-Ext sequence has support terms I ⊓ J, I ⊔ J, and the biproduct of the I- and J-support terms. Thus vanishing of the two outer objects forces vanishing for the supremum support.

Imports1

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisDerivedExtMiddle

Imported by4

theorem

derivedLocalCohomology_sup_isZero_of_mayerVietoris

L30 ↗

EtaleFundamentalGroups.derivedLocalCohomology_sup_isZero_of_mayerVietoris

Documentation

The local-cohomology Mayer--Vietoris vanishing implication obtained from the exact filtered colimit of the derived-Ext powers sequences.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]

Lean source · statement

theorem derivedLocalCohomology_sup_isZero_of_mayerVietoris
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁)
    (hInf : IsZero (derivedLocalCohomology (I ⊓ J) M n₀))
    (hI : IsZero (derivedLocalCohomology I M n₁))
    (hJ : IsZero (derivedLocalCohomology J M n₁)) :
    IsZero (derivedLocalCohomology (I ⊔ J) M n₁)

Module documentation

Mayer--Vietoris vanishing for derived local cohomology

Declarations

derivedLocalCohomology_sup_isZero_of_mayerVietoris