Module

PuncturedSpectrumNormalHypersurfaceLowDegree.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumNormalHypersurfaceLowDegree

3 declarations indexed from sourceView source ↗

Module documentation

Low-degree local cohomology for punctured hypersurfaces

The derived-to-legacy comparison transports the regular-sequence vanishing supplied by Rees' theorem to derived local cohomology. In particular, a regular pair in the maximal ideal kills degree-one derived local cohomology. This is the low-degree source available for a connectedness argument around a principal hypersurface.

Imports3

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyLegacyComparison
Nyll.EtaleFundamentalGroups.Purity.LocalCohomologyRegularSequence
Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

theorem

derivedLocalCohomology_isZero_of_legacy_succ

L32 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_legacy_succ

Documentation

Positive-degree legacy local-cohomology vanishing transports to the derived-Ext colimit through the natural comparison.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
open RingTheory.Sequence
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_isZero_of_legacy_succ
    {R : Type u} [CommRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ)
    (h : IsZero ((localCohomology I (n + 1)).obj M)) :
    IsZero (derivedLocalCohomology I M (n + 1))

theorem

derivedLocalCohomology_isZero_of_isRegular_succ

L47 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_isRegular_succ

Documentation

A regular sequence in the support ideal kills positive-degree derived local cohomology below the length of the sequence.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
open RingTheory.Sequence
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_isZero_of_isRegular_succ
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) [Module.Finite R M]
    (smul_lt : I • (⊤ : Submodule R M) < ⊤)
    (rs : List R) (mem : ∀ r ∈ rs, r ∈ I) (reg : IsRegular M rs)
    (n : ℕ) (hn : n + 1 < rs.length) :
    IsZero (derivedLocalCohomology I M (n + 1))

theorem

derivedLocalCohomology_maximalIdeal_one_isZero_of_isRegular_pair

L60 ↗

EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_one_isZero_of_isRegular_pair

Documentation

A regular pair in the maximal ideal kills degree-one derived local cohomology of the structure module.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
open RingTheory.Sequence
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_maximalIdeal_one_isZero_of_isRegular_pair
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (x y : R) (hx : x ∈ maximalIdeal R) (hy : y ∈ maximalIdeal R)
    (hreg : IsRegular R [x, y]) :
    IsZero
      (derivedLocalCohomology (maximalIdeal R)
        (ModuleCat.of R R) 1)

Module documentation

Low-degree local cohomology for punctured hypersurfaces

Declarations

derivedLocalCohomology_isZero_of_legacy_succ

derivedLocalCohomology_isZero_of_isRegular_succ

derivedLocalCohomology_maximalIdeal_one_isZero_of_isRegular_pair