NYLL
Module

DerivedLocalCohomologyAnnihilatedTop.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyAnnihilatedTop
2 declarations indexed from sourceView source ↗

Module documentation

Top local cohomology of an annihilated coefficient module

A nonzero element of the maximal ideal of a Noetherian local domain can be completed to a system of parameters. Lift a system of parameters from the quotient by that element; regularity gives the required dimension drop.

If this first parameter annihilates the coefficient module, the sharpened generator bound gives vanishing in the top degree. This is the coefficient vanishing input for multiplication on top local cohomology, in every finite dimension.

Imports6
Imported by3

Declarations

theorem

exists_parameter_list_radical_eq_maximalIdeal_of_ringKrullDim_eq_succ

L37 ↗
EtaleFundamentalGroups.exists_parameter_list_radical_eq_maximalIdeal_of_ringKrullDim_eq_succ
Documentation

A nonzero nonunit in a local domain of dimension d + 1 extends to a list of d + 1 parameters with maximal radical.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem exists_parameter_list_radical_eq_maximalIdeal_of_ringKrullDim_eq_succ
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (d : ℕ) (hdim : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞))
    (x : R) (hx0 : x ≠ 0) (hxmem : x ∈ maximalIdeal R) :
    ∃ xs : List R, xs.length = d ∧
      (Ideal.ofList (x :: xs)).radical = maximalIdeal R
theorem

derivedLocalCohomology_maximalIdeal_isZero_succ_of_smul_id_eq_zero

L92 ↗
EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_isZero_succ_of_smul_id_eq_zero
Documentation

In every positive finite dimension, a nonzero member of the maximal ideal annihilating the coefficients forces top local cohomology to vanish.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem derivedLocalCohomology_maximalIdeal_isZero_succ_of_smul_id_eq_zero
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (d : ℕ) (hdim : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞))
    (x : R) (hx0 : x ≠ 0) (hxmem : x ∈ maximalIdeal R)
    (M : ModuleCat.{u} R) (hx : x • 𝟙 M = 0) :
    IsZero (derivedLocalCohomology (maximalIdeal R) M (d + 1))

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