Module

DerivedLocalCohomologyProjectiveDimension.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyProjectiveDimension

2 declarations indexed from sourceView source ↗

Module documentation

Projective-dimension vanishing for derived local cohomology

Uniform projective-dimension bounds make every object of the derived Ext ideal-powers diagram trivial. This gives the derived-colimit counterpart of the existing vanishing results for Mathlib's legacy local-cohomology object.

Imports2

Imported by3

theorem

derivedLocalCohomology_isZero_of_quotientPowers_hasProjectiveDimensionLT

L29 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_quotientPowers_hasProjectiveDimensionLT

Documentation

A uniform projective-dimension bound on the ideal-power quotients forces the corresponding derived local-cohomology colimit to vanish.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_isZero_of_quotientPowers_hasProjectiveDimensionLT
    {R : Type u} [CommRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) (d i : ℕ) (hdi : d ≤ i)
    (hpd : ∀ n : ℕ,
      HasProjectiveDimensionLT (ModuleCat.of R (R ⧸ I ^ n)) d) :
    IsZero (derivedLocalCohomology I M i)

theorem

derivedLocalCohomology_span_singleton_isZero_of_isSMulRegular

L43 ↗

EtaleFundamentalGroups.derivedLocalCohomology_span_singleton_isZero_of_isSMulRegular