NYLL
Module

DerivedLocalCohomologySupportDimensionVanishing.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologySupportDimensionVanishing
2 declarations indexed from sourceView source ↗

Module documentation

Vanishing above the support dimension

Degree induction and a prime filtration reduce finite coefficient modules to prime quotients. Either the support ideal annihilates such a quotient, or it contains a regular scalar in the maximal ideal. Quotienting by that scalar lowers support dimension. Vanishing in the preceding degree makes the scalar injective on local cohomology, and power torsion then forces that local cohomology to vanish.

Imports16
Imported by4

Declarations

theorem

derivedLocalCohomology_isZero_of_supportDim_lt

L46 ↗
EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_supportDim_lt
Documentation

Local cohomology of a finite module over a Noetherian local ring, with any support ideal, vanishes above the dimension of the module's support.

Source context 5 commands

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

namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem derivedLocalCohomology_isZero_of_supportDim_lt
    (I : Ideal R) (M : ModuleCat.{u} R) [Module.Finite R M] (n : ℕ)
    (hdim : Module.supportDim R M < (n : WithBot ℕ∞)) :
    IsZero (derivedLocalCohomology I M n)
theorem

derivedLocalCohomology_maximalIdeal_isZero_of_supportDim_lt

L153 ↗
EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_isZero_of_supportDim_lt
Documentation

Maximal-support local cohomology of a finite module over a Noetherian local ring vanishes in every degree above the dimension of its support.

Source context 5 commands

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

namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem derivedLocalCohomology_maximalIdeal_isZero_of_supportDim_lt
    (M : ModuleCat.{u} R) [Module.Finite R M] (n : ℕ)
    (hdim : Module.supportDim R M < (n : WithBot ℕ∞)) :
    IsZero (derivedLocalCohomology (maximalIdeal R) M n)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.