NYLL
Module

RegularCartier.lean

Nyll.SchemeTheory.Divisors.RegularCartier
2 declarations indexed from sourceView source ↗

Module documentation

Ambient regularity along a regular Cartier divisor

A regular effective Cartier divisor in a locally Noetherian scheme forces the ambient local rings along its support to be regular. The proof uses the actual quotient description of the divisor's stalk and the regularity lifting theorem for a quotient by a non-zero-divisor.

This supplies the regular-local-ring step in the proof of Stacks Project, Tag 0EYE, using the one-element case of Tag 00NU. The stalk-generator lemma was moved here from EtaleFundamentalGroups.LocalGeometry.HeightOne.CartierComponentStalkDVR with its statement, proof, and authorship preserved.

Imports8
Imported by5

Declarations

theorem

exists_regular_stalkIdeal_generator

L43 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.exists_regular_stalkIdeal_generator
Documentation

An effective Cartier ideal has a regular generator in every stalk. The affine Cartier equation remains regular because the germ map is a flat localization; the defining affine ideal maps to the stalk ideal.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem IsEffectiveCartier.exists_regular_stalkIdeal_generator
    {X : Scheme.{u}} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier)
    (x : X) :
    ∃ a : X.presheaf.stalk x, IsRegular a ∧ I.stalkIdeal x = Ideal.span {a}
theorem

isAmbientRegularAlongSupport_of_regular_subscheme

L64 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.isAmbientRegularAlongSupport_of_regular_subscheme
Documentation

If the closed subscheme of an effective Cartier ideal is regular, then the ambient scheme is regular at each point of its support.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem IsEffectiveCartier.isAmbientRegularAlongSupport_of_regular_subscheme
    {X : Scheme.{u}} [IsLocallyNoetherian X] {I : X.IdealSheafData}
    (hI : I.IsEffectiveCartier)
    (hregular : ∀ z : I.subscheme,
      IsRegularLocalRing (I.subscheme.presheaf.stalk z)) :
    I.IsAmbientRegularAlongSupport

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