Module

DerivedLocalCohomologySupportDimensionZero.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologySupportDimensionZero

3 declarations indexed from sourceView source ↗

Module documentation

Degree-zero nonvanishing for zero-dimensional coefficients

The support of a zero-dimensional finite module over a local ring is the closed point. A power of the maximal ideal therefore annihilates it, and degree-zero local cohomology evaluates isomorphically onto the module.

Imports9

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDegreeZeroModule
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyModule
Mathlib.Algebra.Category.Grp.Zero
Mathlib.Algebra.Module.Submodule.Equiv
Mathlib.RingTheory.Finiteness.Ideal
Mathlib.RingTheory.KrullDimension.Module
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Spectrum.Prime.Basic
Mathlib.RingTheory.Support

Imported by2

theorem

exists_maximalIdeal_pow_le_annihilator_of_supportDim_eq_zero

L37 ↗

EtaleFundamentalGroups.exists_maximalIdeal_pow_le_annihilator_of_supportDim_eq_zero

Documentation

Zero-dimensional finite coefficients are killed by a single power of the maximal ideal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem exists_maximalIdeal_pow_le_annihilator_of_supportDim_eq_zero
    (M : ModuleCat.{u} R) [Module.Finite R M]
    (hdim : Module.supportDim R M = 0) :
    ∃ k : ℕ, maximalIdeal R ^ k ≤ Module.annihilator R M

def

derivedLocalCohomologyZeroEquivOfSupportDimEqZero

L53 ↗

EtaleFundamentalGroups.derivedLocalCohomologyZeroEquivOfSupportDimEqZero

Documentation

Evaluation identifies degree-zero maximal-support cohomology with finite zero-dimensional coefficients.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

def derivedLocalCohomologyZeroEquivOfSupportDimEqZero
    (M : ModuleCat.{u} R) [Module.Finite R M]
    (hdim : Module.supportDim R M = 0) :
    derivedLocalCohomologyModule (maximalIdeal R) M 0 ≃ₗ[R] M

theorem

derivedLocalCohomology_maximalIdeal_not_isZero_of_supportDim_eq_zero

L65 ↗

EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_not_isZero_of_supportDim_eq_zero

Documentation

A finite module of support dimension zero has nonzero degree-zero maximal-support local cohomology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem derivedLocalCohomology_maximalIdeal_not_isZero_of_supportDim_eq_zero
    (M : ModuleCat.{u} R) [Module.Finite R M]
    (hdim : Module.supportDim R M = 0) :
    ¬ IsZero (derivedLocalCohomology (maximalIdeal R) M 0)

Module documentation

Degree-zero nonvanishing for zero-dimensional coefficients

Declarations

exists_maximalIdeal_pow_le_annihilator_of_supportDim_eq_zero

derivedLocalCohomologyZeroEquivOfSupportDimEqZero

derivedLocalCohomology_maximalIdeal_not_isZero_of_supportDim_eq_zero