Module

DerivedLocalCohomologyGeneratorCountDomain.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyGeneratorCountDomain

4 declarations indexed from sourceView source ↗

Module documentation

Generator-count vanishing over a local domain

For a finite list in a Noetherian local domain, derived local cohomology supported on the ideal generated by the list vanishes in degrees strictly larger than the list length. If one generator is a unit, the support is the unit ideal; otherwise every generator lies in the maximal ideal.

The proof avoids a missing general comparison with a Cech complex. A nonzero element of a domain is regular, so the one-generator case follows from the existing projective-dimension calculation. Mayer--Vietoris then adds generators one at a time. Its intersection term is replaced, using radical invariance, by the product ideal generated by the list of products with the new generator. This list is shorter, so strong induction closes.

Imports4

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyMayerVietoris
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyProjectiveDimension
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyRadical
Mathlib.RingTheory.Regular.RegularSequence

Imported by7

theorem

span_singleton_mul_ofList

L39 ↗

EtaleFundamentalGroups.span_singleton_mul_ofList

Documentation

The ideal generated by multiplying every member of a list by one fixed element is the product of the corresponding principal ideal with the ideal generated by the original list.

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 · full declaration

theorem span_singleton_mul_ofList
    {R : Type u} [CommRing R] (x : R) (xs : List R) :
    Ideal.span {x} * Ideal.ofList xs =
      Ideal.ofList (xs.map fun y ↦ x * y) := by
  unfold Ideal.ofList
  rw [Ideal.span_mul_span, Set.singleton_mul]
  congr 1
  ext z
  simp

theorem

derivedLocalCohomology_bot_isZero

L51 ↗

EtaleFundamentalGroups.derivedLocalCohomology_bot_isZero

Documentation

Derived local cohomology supported at the zero ideal vanishes in every positive degree.

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_bot_isZero
    {R : Type u} [CommRing R] [Nontrivial R]
    (M : ModuleCat.{u} R) (i : ℕ) (hi : 1 ≤ i) :
    IsZero (derivedLocalCohomology (⊥ : Ideal R) M i)

theorem

derivedLocalCohomology_top_isZero

L79 ↗

EtaleFundamentalGroups.derivedLocalCohomology_top_isZero

Documentation

Derived local cohomology supported at the unit ideal is zero in every degree.

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_top_isZero
    {R : Type u} [CommRing R]
    (M : ModuleCat.{u} R) (i : ℕ) :
    IsZero (derivedLocalCohomology (⊤ : Ideal R) M i)

theorem

derivedLocalCohomology_ofList_isZero_of_isDomain

L94 ↗

EtaleFundamentalGroups.derivedLocalCohomology_ofList_isZero_of_isDomain

Documentation

In a Noetherian local domain, local cohomology supported on an ideal listed by xs vanishes above the number of listed generators. Repetitions and zero entries are allowed.

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_ofList_isZero_of_isDomain
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (xs : List R)
    (M : ModuleCat.{u} R) (i : ℕ) (hi : xs.length < i) :
    IsZero (derivedLocalCohomology (Ideal.ofList xs) M i)

Module documentation

Generator-count vanishing over a local domain

Declarations

span_singleton_mul_ofList

derivedLocalCohomology_bot_isZero

derivedLocalCohomology_top_isZero

derivedLocalCohomology_ofList_isZero_of_isDomain