NYLL
Module

DerivedLocalCohomologyDimensionOneHL.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDimensionOneHL
1 declaration indexed from sourceView source ↗

Module documentation

Hartshorne--Lichtenbaum vanishing in dimension one

In a one-dimensional local domain, every nonzero element has principal radical containing the maximal ideal. Consequently, a proper radical ideal different from the maximal ideal contains no nonzero element and is the zero ideal. Positive-degree vanishing for zero support then proves the dimension-one Hartshorne--Lichtenbaum source.

Imports2
Imported by1

Declarations

theorem

derivedLocalCohomology_isZero_of_isRadical_ne_maximalIdeal_of_ringKrullDim_eq_one

L30 ↗
EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_isRadical_ne_maximalIdeal_of_ringKrullDim_eq_one
Documentation

Hartshorne--Lichtenbaum vanishing in dimension one for a radical support different from the maximal ideal.

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_isZero_of_isRadical_ne_maximalIdeal_of_ringKrullDim_eq_one
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    (hdim : ringKrullDim R = 1)
    (J : Ideal R) (hJradical : J.IsRadical)
    (hJnonmax : J ≠ maximalIdeal R) :
    IsZero (derivedLocalCohomology J (ModuleCat.of R R) 1)

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