NYLL
Module

CompleteLocalTopCohomologyDual.lean

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

Module documentation

The dual of top local cohomology over a complete local domain

Every nonzero scalar acts surjectively on positive top local cohomology of a local domain. Its linear dual is therefore torsion-free. For a complete domain, top nonvanishing and separation by an injective module containing the residue field also make this dual nonzero. Artinianness and maximal-ideal-power torsion make the dual into the residue-field injective hull finitely generated.

Imports16
Imported by3

Declarations

theorem

isTorsionFree_linearMap_topLocalCohomology

L45 ↗
EtaleFundamentalGroups.Purity.isTorsionFree_linearMap_topLocalCohomology
Documentation

The linear dual of positive top local cohomology is torsion-free, because every nonzero scalar is surjective on the original module.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem isTorsionFree_linearMap_topLocalCohomology
    (E : Type v) [AddCommGroup E] [Module R E] (d : ℕ)
    (hdim : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞)) :
    Module.IsTorsionFree R
      (derivedLocalCohomologyModule (maximalIdeal R) (ModuleCat.of R R) (d + 1) →ₗ[R] E)
theorem

nontrivial_linearMap_topLocalCohomology

L70 ↗
EtaleFundamentalGroups.Purity.nontrivial_linearMap_topLocalCohomology
Documentation

The dual with values in an injective module containing the residue field detects the nonzero top cohomology of a complete local domain.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsDomain R] in
Lean source · statement
theorem nontrivial_linearMap_topLocalCohomology
    [IsAdicComplete (maximalIdeal R) R]
    {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (d : ℕ) (hdim : ringKrullDim R = (d : WithBot ℕ∞)) :
    Nontrivial
      (derivedLocalCohomologyModule (maximalIdeal R) (ModuleCat.of R R) d →ₗ[R] E)
theorem

finite_linearMap_localCohomology_maximalIdeal

L95 ↗
EtaleFundamentalGroups.Purity.finite_linearMap_localCohomology_maximalIdeal
Documentation

The dual of maximal-support local cohomology with values in the residue-field injective hull is finite over a complete local ring.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsDomain R] in
Lean source · statement
theorem finite_linearMap_localCohomology_maximalIdeal
    [IsAdicComplete (maximalIdeal R) R]
    {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i))
    (M : ModuleCat.{u} R) [Module.Finite R M] (d : ℕ) :
    Module.Finite R
      (derivedLocalCohomologyModule (maximalIdeal R) M d →ₗ[R] E)

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