EtaleFundamentalGroups.localCohomology_isZero_of_isRegular
If an ideal contains a regular sequence of length greater than i, then local cohomology in degree i vanishes.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
open RingTheory.Sequence
namespace EtaleFundamentalGroups
universe uLean source · statement
theorem localCohomology_isZero_of_isRegular
{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)
(i : ℕ) (hi : i < rs.length) :
IsZero ((localCohomology I i).obj M)