NYLL
Module

DerivedLocalCohomologySupportDimensionNonvanishing.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologySupportDimensionNonvanishing
3 declarations indexed from sourceView source ↗

Module documentation

Top local-cohomology nonvanishing for finite coefficients

Over a complete Noetherian local ring, a finite module of finite support dimension has nonzero local cohomology in that dimension. In positive dimension the top local-cohomology module is not finitely generated.

The two conclusions are proved together by induction on dimension. Removing the maximal-ideal-primary component preserves positive support dimension and positive local cohomology. A regular scalar can then be chosen whose quotient on the preceding Artinian cohomology has finite length. Vanishing in the top degree would contradict the induction hypothesis on the coefficient scalar quotient. Finite generation in the top degree would force that vanishing by Nakayama's lemma.

Imports20
Imported by3

Declarations

theorem

topLocalCohomology_nonzero_and_notFinite

L54 ↗
EtaleFundamentalGroups.topLocalCohomology_nonzero_and_notFinite
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 topLocalCohomology_nonzero_and_notFinite
    (M : ModuleCat.{u} R) [Module.Finite R M] (d : ℕ)
    (hdim : Module.supportDim R M = (d : WithBot ℕ∞)) :
    (¬ IsZero (derivedLocalCohomology (maximalIdeal R) M d)) ∧
      (d ≠ 0 → ¬ Module.Finite R
        (derivedLocalCohomologyModule (maximalIdeal R) M d))
theorem

derivedLocalCohomology_maximalIdeal_not_isZero_of_supportDim_eq

L139 ↗
EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_not_isZero_of_supportDim_eq
Documentation

A finite module of finite support dimension has nonzero local cohomology in that degree over a complete Noetherian local ring.

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 derivedLocalCohomology_maximalIdeal_not_isZero_of_supportDim_eq
    (M : ModuleCat.{u} R) [Module.Finite R M] (d : ℕ)
    (hdim : Module.supportDim R M = (d : WithBot ℕ∞)) :
    ¬ IsZero (derivedLocalCohomology (maximalIdeal R) M d)
theorem

not_moduleFinite_derivedLocalCohomologyModule_maximalIdeal_of_supportDim_eq

L147 ↗
EtaleFundamentalGroups.not_moduleFinite_derivedLocalCohomologyModule_maximalIdeal_of_supportDim_eq
Documentation

Top local cohomology in positive finite support dimension is not a finite module over a complete Noetherian local ring.

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 not_moduleFinite_derivedLocalCohomologyModule_maximalIdeal_of_supportDim_eq
    (M : ModuleCat.{u} R) [Module.Finite R M] (d : ℕ) (hd : 0 < d)
    (hdim : Module.supportDim R M = (d : WithBot ℕ∞)) :
    ¬ Module.Finite R (derivedLocalCohomologyModule (maximalIdeal R) M d)

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