EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_isZero_succ_of_finite_of_regular
Finite top local cohomology vanishes when the finite coefficient module admits a regular scalar in the maximal ideal.
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_succ_of_finite_of_regular
(M : ModuleCat.{u} R) [Module.Finite R M] (d : ℕ)
(hdim : Module.supportDim R M = ((d + 1 : ℕ) : WithBot ℕ∞))
(x : R) (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular M x)
[Module.Finite R (derivedLocalCohomologyModule (maximalIdeal R) M (d + 1))] :
IsZero (derivedLocalCohomology (maximalIdeal R) M (d + 1))