NYLL
Module

DerivedLocalCohomologyArtinian.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyArtinian
1 declaration indexed from sourceView source ↗

Module documentation

Artinianness of maximal-support local cohomology

Induction on degree is combined with a prime filtration of the finite coefficient module. Residue-field factors have no positive local cohomology. Every other prime factor has a regular scalar in the maximal ideal, and its scalar quotient reduces the degree. The coefficient exact sequence preserves Artinianness under finite extensions.

Imports12
Imported by4

Declarations

theorem

isArtinian_derivedLocalCohomologyModule_maximalIdeal

L42 ↗
EtaleFundamentalGroups.isArtinian_derivedLocalCohomologyModule_maximalIdeal
Documentation

Maximal-support local cohomology of a finite module over a complete Noetherian local ring is Artinian in every degree.

Source context 6 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]
variable [IsAdicComplete (maximalIdeal R) R]
Lean source · statement
theorem isArtinian_derivedLocalCohomologyModule_maximalIdeal
    (M : ModuleCat.{u} R) [Module.Finite R M] (n : ℕ) :
    IsArtinian R (derivedLocalCohomologyModule (maximalIdeal R) M n)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.