Module

StrictNormalCrossingsLocalCohomology.lean

Nyll.EtaleFundamentalGroups.Purity.StrictNormalCrossingsLocalCohomology

2 declarations indexed from sourceView source ↗

Module documentation

Local cohomology at strict-normal-crossings points

The regular system of parameters supplied by a strict-normal-crossings chart is a regular sequence generating the maximal ideal of the local ring. This file feeds that actual sequence into the regular-sequence vanishing theorem for local cohomology. The result is valid in every dimension represented by the parameter family.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

theorem

localCohomology_maximalIdeal_isZero_of_regularSystemOfParameters

L32 ↗

EtaleFundamentalGroups.localCohomology_maximalIdeal_isZero_of_regularSystemOfParameters

Documentation

A regular system of d parameters in a Noetherian local ring forces the structure module's local cohomology supported at the maximal ideal to vanish in every degree strictly below d.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
open RingTheory.Sequence
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem localCohomology_maximalIdeal_isZero_of_regularSystemOfParameters
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {d : ℕ} (t : Fin d → R)
    (ht : AlgebraicGeometry.Scheme.IsRegularSystemOfParameters t)
    (i : ℕ) (hi : i < d) :
    IsZero
      ((localCohomology (IsLocalRing.maximalIdeal R) i).obj
        (ModuleCat.of R R))

theorem

exists_parameterChart_localCohomology_isZero

L69 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossingsAt.exists_parameterChart_localCohomology_isZero

Documentation

A strict-normal-crossings point supplies, without a dimension-two restriction, a regular parameter chart whose full range of low-degree local cohomology groups at the stalk's maximal ideal vanishes.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open RingTheory.Sequence
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData} {x : X}

Lean source · full declaration

theorem IsStrictNormalCrossingsAt.exists_parameterChart_localCohomology_isZero
    (hI : I.IsStrictNormalCrossingsAt x) :
    let R := X.presheaf.stalk x
    ∃ (d r : ℕ) (t : Fin d → R),
      0 < r ∧ ∃ (hr : r ≤ d),
        AlgebraicGeometry.Scheme.IsRegularSystemOfParameters t ∧
          I.stalkIdeal x =
            Ideal.span
              {AlgebraicGeometry.Scheme.initialParameterProduct t r hr} ∧
          ∀ i : ℕ, i < d →
            IsZero
              ((localCohomology (IsLocalRing.maximalIdeal R) i).obj
                (ModuleCat.of R R)) := by
  dsimp only
  let R := X.presheaf.stalk x
  let hregular : IsRegularLocalRing R := hI.1
  let : IsLocalRing R := hregular.toIsLocalRing
  let : IsNoetherianRing R := hregular.toIsNoetherian
  obtain ⟨d, r, t, hrpos, hr, ht, hideal⟩ := hI.2
  refine ⟨d, r, t, hrpos, hr, ht, hideal, ?_⟩
  intro i hi
  exact
    EtaleFundamentalGroups.localCohomology_maximalIdeal_isZero_of_regularSystemOfParameters
      t ht i hi

Module documentation

Local cohomology at strict-normal-crossings points

Declarations

localCohomology_maximalIdeal_isZero_of_regularSystemOfParameters

exists_parameterChart_localCohomology_isZero