Module

DerivedLocalCohomologyArtinianZero.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyArtinianZero

2 declarations indexed from sourceView source ↗

Module documentation

Finite length in degree zero

Degree-zero local cohomology embeds in its finite coefficient module. Noetherianity makes it finite, and its maximal-ideal-power torsion then gives finite length. This is the base of the Artinianness induction.

Imports6

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDegreeZeroModule
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyModule
Nyll.EtaleFundamentalGroups.Purity.FinitePowerTorsionLength
Mathlib.RingTheory.FiniteLength
Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
Mathlib.RingTheory.Noetherian.Basic

Imported by3

theorem

isFiniteLength_derivedLocalCohomologyModule_maximalIdeal_zero

L30 ↗

EtaleFundamentalGroups.isFiniteLength_derivedLocalCohomologyModule_maximalIdeal_zero

Documentation

Degree-zero local cohomology of a finite module over a Noetherian local ring has finite length.

Source context 3 commands

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

namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem isFiniteLength_derivedLocalCohomologyModule_maximalIdeal_zero
    (M : ModuleCat.{u} R) [Module.Finite R M] :
    IsFiniteLength R
      (derivedLocalCohomologyModule (IsLocalRing.maximalIdeal R) M 0)

theorem

isArtinian_derivedLocalCohomologyModule_maximalIdeal_zero

L45 ↗

EtaleFundamentalGroups.isArtinian_derivedLocalCohomologyModule_maximalIdeal_zero