NYLL
Module

DerivedLocalCohomologyDimensionTwoAnnihilated.lean

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

Module documentation

Dimension-two local cohomology with an annihilated coefficient module

The parameter-pair and coefficient-vanishing results are the two-dimensional specializations of the general parameter-list construction and annihilated-coefficient top-degree bound.

Imports2
Imported by1

Declarations

theorem

exists_parameter_pair_radical_eq_maximalIdeal_of_ringKrullDim_eq_two

L28 ↗
EtaleFundamentalGroups.exists_parameter_pair_radical_eq_maximalIdeal_of_ringKrullDim_eq_two
Documentation

In an exact two-dimensional Noetherian local domain, a nonzero element of the maximal ideal extends to a pair 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_pair_radical_eq_maximalIdeal_of_ringKrullDim_eq_two
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (x : R) (hx0 : x ≠ 0) (hxmem : x ∈ maximalIdeal R) :
    ∃ y : R,
      (Ideal.span {x} ⊔ Ideal.span {y}).radical = maximalIdeal R
theorem

derivedLocalCohomology_maximalIdeal_isZero_two_of_smul_id_eq_zero

L45 ↗
EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_isZero_two_of_smul_id_eq_zero
Documentation

In exact dimension two, a coefficient module annihilated by a nonzero member of the maximal ideal has vanishing degree-two maximal-support derived local cohomology.

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_two_of_smul_id_eq_zero
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (x : R) (hx0 : x ≠ 0) (hxmem : x ∈ maximalIdeal R)
    (M : ModuleCat.{u} R) (hx : x • 𝟙 M = 0) :
    IsZero
      (derivedLocalCohomology (maximalIdeal R) M 2)

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