NYLL
Module

CompleteLocalCohomologyDualSupportDimension.lean

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalCohomologyDualSupportDimension
5 declarations indexed from sourceView source ↗

Module documentation

Support dimension of dual local cohomology

The dual of degree n maximal-support local cohomology of finite coefficients has support dimension at most n. The proof uses the coefficient long exact sequence and the dimension inequality for a scalar quotient. In degree zero a uniform maximal-ideal power kills the cohomology and its dual. In positive degree the primary component is removed before choosing a regular scalar.

Imports18
Imported by2

Declarations

theorem

supportDim_le_zero_of_maximalIdeal_pow_le_annihilator

L47 ↗
EtaleFundamentalGroups.Purity.supportDim_le_zero_of_maximalIdeal_pow_le_annihilator
Source context 6 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem supportDim_le_zero_of_maximalIdeal_pow_le_annihilator
    (N : Type u) [AddCommGroup N] [Module R N] [Module.Finite R N]
    (k : ℕ) (hk : maximalIdeal R ^ k ≤ Module.annihilator R N) :
    Module.supportDim R N ≤ 0
theorem

supportDim_linearMap_localCohomology_zero_le_zero

L65 ↗
EtaleFundamentalGroups.Purity.supportDim_linearMap_localCohomology_zero_le_zero
Source context 7 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem supportDim_linearMap_localCohomology_zero_le_zero
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i))
    (M : ModuleCat.{u} R) [Module.Finite R M] :
    Module.supportDim R
      (derivedLocalCohomologyModule (maximalIdeal R) M 0 →ₗ[R] E) ≤ 0
theorem

supportDim_linearMap_localCohomology_maximalIdeal_le

L89 ↗
EtaleFundamentalGroups.Purity.supportDim_linearMap_localCohomology_maximalIdeal_le
Documentation

The dual of maximal-support local cohomology in degree n has support dimension at most n.

Source context 7 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem supportDim_linearMap_localCohomology_maximalIdeal_le
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i))
    (M : ModuleCat.{u} R) [Module.Finite R M] (n : ℕ) :
    Module.supportDim R
      (derivedLocalCohomologyModule (maximalIdeal R) M n →ₗ[R] E) ≤
        (n : WithBot ℕ∞)
theorem

exists_ne_zero_annihilator_linearMap_localCohomology_of_lt_dim

L144 ↗
EtaleFundamentalGroups.Purity.exists_ne_zero_annihilator_linearMap_localCohomology_of_lt_dim
Documentation

Below the ring dimension, a single nonzero scalar annihilates the dual cohomology. For a domain this supplies the torsion deficiency modules used in the truncation argument.

Source context 7 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem exists_ne_zero_annihilator_linearMap_localCohomology_of_lt_dim
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i))
    (M : ModuleCat.{u} R) [Module.Finite R M] (n : ℕ)
    (hn : (n : WithBot ℕ∞) < ringKrullDim R) :
    ∃ a : R, a ≠ 0 ∧ ∀ f :
      derivedLocalCohomologyModule (maximalIdeal R) M n →ₗ[R] E, a • f = 0
theorem

exists_ne_zero_annihilator_lower_linearMap_localCohomology

L166 ↗
EtaleFundamentalGroups.Purity.exists_ne_zero_annihilator_lower_linearMap_localCohomology
Documentation

Over a domain the finitely many lower dual cohomology modules have one common nonzero annihilator.

Source context 7 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem exists_ne_zero_annihilator_lower_linearMap_localCohomology
    [IsDomain R]
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i))
    (M : ModuleCat.{u} R) [Module.Finite R M] (d : ℕ)
    (hdim : (d : WithBot ℕ∞) ≤ ringKrullDim R) :
    ∃ a : R, a ≠ 0 ∧ ∀ n < d, ∀ f :
      derivedLocalCohomologyModule (maximalIdeal R) M n →ₗ[R] E, a • f = 0

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