Module

DerivedLocalCohomologyAnnihilatedGenerators.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyAnnihilatedGenerators

1 declaration indexed from sourceView source ↗

Module documentation

Generator-count vanishing with an annihilated coefficient module

If one generator of the support ideal annihilates the coefficient module, local cohomology vanishes above the number of remaining generators. The proof uses strong induction on that number. Mayer--Vietoris removes one remaining generator; its intersection term has the same radical as the product ideal, which again has an annihilating generator and fewer remaining generators. The induction starts with principal-support degree-one vanishing for an annihilated module.

Imports5

Imported by2

theorem

derivedLocalCohomology_ofList_cons_isZero_of_smul_id_eq_zero

L37 ↗

EtaleFundamentalGroups.derivedLocalCohomology_ofList_cons_isZero_of_smul_id_eq_zero

Documentation

Over a Noetherian local domain, an annihilating support generator lowers by one the generator-count bound for local cohomology of the coefficient module. No regularity or nonzero assumption on the annihilating generator is needed.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_ofList_cons_isZero_of_smul_id_eq_zero
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (x : R) (xs : List R) (M : ModuleCat.{u} R)
    (hx : x • 𝟙 M = 0) (i : ℕ) (hi : xs.length < i) :
    IsZero (derivedLocalCohomology (Ideal.ofList (x :: xs)) M i)

Module documentation

Generator-count vanishing with an annihilated coefficient module

Declarations

derivedLocalCohomology_ofList_cons_isZero_of_smul_id_eq_zero