Module

LocalCohomologyProjectiveDimension.lean

Nyll.EtaleFundamentalGroups.Purity.LocalCohomologyProjectiveDimension

3 declarations indexed from sourceView source ↗

Module documentation

High-degree local-cohomology vanishing from projective dimension

Local cohomology is a colimit of Ext groups against the quotients by powers of its support ideal. A uniform projective-dimension bound for those quotients therefore gives high-degree vanishing. For a principal ideal generated by a regular element, every positive power quotient has projective dimension one, so all local cohomology in degree at least two vanishes.

The principal case is the cohomological-dimension input used in the complete-local connectedness argument for punctured hypersurfaces.

Imports3

Mathlib.RingTheory.Regular.ProjectiveDimension
Nyll.EtaleFundamentalGroups.Purity.DerivedExtLegacyComparison
Nyll.EtaleFundamentalGroups.Purity.LocalCohomologyExtVanishing

Imported by3

theorem

localCohomology_isZero_of_quotientPowers_hasProjectiveDimensionLT

L35 ↗

EtaleFundamentalGroups.localCohomology_isZero_of_quotientPowers_hasProjectiveDimensionLT

Documentation

Local cohomology in degree i vanishes when every ideal-power quotient has projective dimension strictly less than a fixed bound d ≤ i.

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 localCohomology_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 ((localCohomology I i).obj M)

theorem

quotient_span_singleton_hasProjectiveDimensionLT_two

L53 ↗

EtaleFundamentalGroups.quotient_span_singleton_hasProjectiveDimensionLT_two

Documentation

A quotient by a regular element in the maximal ideal has projective dimension strictly less than two.

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 quotient_span_singleton_hasProjectiveDimensionLT_two
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (x : R) (hxreg : IsSMulRegular R x)
    (hxmem : x ∈ IsLocalRing.maximalIdeal R) :
    HasProjectiveDimensionLT
      (ModuleCat.of R (R ⧸ Ideal.span {x})) 2

theorem

localCohomology_span_singleton_isZero_of_isSMulRegular

L85 ↗

EtaleFundamentalGroups.localCohomology_span_singleton_isZero_of_isSMulRegular

Documentation

Local cohomology supported on a principal regular ideal vanishes in degrees at least two.

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 localCohomology_span_singleton_isZero_of_isSMulRegular
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (x : R) (hxreg : IsSMulRegular R x)
    (hxmem : x ∈ IsLocalRing.maximalIdeal R)
    (M : ModuleCat.{u} R) (i : ℕ) (hi : 2 ≤ i) :
    IsZero ((localCohomology (Ideal.span {x}) i).obj M)

Module documentation

High-degree local-cohomology vanishing from projective dimension

Declarations

localCohomology_isZero_of_quotientPowers_hasProjectiveDimensionLT

quotient_span_singleton_hasProjectiveDimensionLT_two

localCohomology_span_singleton_isZero_of_isSMulRegular