Module

DerivedLocalCohomologyTopDegreeBound.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyTopDegreeBound

2 declarations indexed from sourceView source ↗

Module documentation

Upper degree bound for maximal-support derived local cohomology

In a Noetherian local domain of finite Krull dimension d, choose d parameters whose generated ideal has maximal radical. Generator-count vanishing for that ideal, followed by radical invariance, gives vanishing of maximal-support derived local cohomology in every degree strictly above d.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

theorem

derivedLocalCohomology_maximalIdeal_isZero_of_ringKrullDim_lt

L29 ↗

EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_isZero_of_ringKrullDim_lt

Documentation

Maximal-support derived local cohomology of a Noetherian local domain vanishes strictly above its finite Krull dimension.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_maximalIdeal_isZero_of_ringKrullDim_lt
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (d i : ℕ) (hdim : ringKrullDim R = (d : WithBot ℕ∞)) (hi : d < i) :
    IsZero
      (derivedLocalCohomology (maximalIdeal R) (ModuleCat.of R R) i)

theorem

derivedLocalCohomology_maximalIdeal_isZero_succ_of_ringKrullDim_eq

L51 ↗

EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_isZero_succ_of_ringKrullDim_eq