Documentation

TauCeti.AlgebraicGeometry.Scheme.Regular.Scheme

Regular schemes #

A scheme is regular if it is locally Noetherian and every local ring is regular. We use the stalkwise characterization in Stacks, Lemma 28.9.2 (02IT). Regularity is preserved under open immersions and smooth morphisms and can be checked on affine neighbourhoods of each point. It is also equivalent to regularity of every affine-open section ring. The spectrum of a ring is regular exactly when the ring is regular, and regular schemes are normal. Normality follows from the affine criterion and the ring-level theorem TauCeti.IsRegularRing.isIntegrallyClosed. Conversely, in dimension at most one a locally Noetherian normal scheme is regular, since its local rings are fields or discrete valuation rings.

Main declarations #

References #

source
class TauCeti.AlgebraicGeometry.IsRegular (X : AlgebraicGeometry.Scheme) extends AlgebraicGeometry.IsLocallyNoetherian X :
Prop

A regular scheme is locally Noetherian and has regular local rings. This is condition (2) in Stacks, Lemma 28.9.2 (02IT).

Instances
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.isRegular_iff_forall_stalk {X : AlgebraicGeometry.Scheme} :
    IsRegular X ↔ AlgebraicGeometry.IsLocallyNoetherian X ∧ ∀ (x : ↥X), IsRegularLocalRing ↑(X.presheaf.stalk x)

    A scheme is regular iff it is locally Noetherian and every stalk is a regular local ring.

    source
    theorem TauCeti.AlgebraicGeometry.IsRegular.of_isOpenImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [IsRegular Y] :
    IsRegular X

    The source of an open immersion into a regular scheme is regular.

    source
    theorem TauCeti.AlgebraicGeometry.IsRegular.of_smooth {X target : AlgebraicGeometry.Scheme} (morphism : X ⟶ target) [AlgebraicGeometry.Smooth morphism] [IsRegular target] :
    IsRegular X

    The source of a smooth morphism into a regular scheme is regular. This is the preservation direction of Stacks, Lemma 35.18.4 (036D).

    source
    theorem TauCeti.AlgebraicGeometry.IsRegular.of_isIso_morphismRestrict {Y Y' B : AlgebraicGeometry.Scheme} [IsRegular Y] [AlgebraicGeometry.IsLocallyNoetherian Y'] (ι : Y ⟶ Y') [AlgebraicGeometry.IsOpenImmersion ι] (f' : Y' ⟶ B) (V : B.Opens) [CategoryTheory.IsIso (f' ∣_ V)] (hcov : AlgebraicGeometry.Scheme.Hom.opensRange ι ⊔ (TopologicalSpace.Opens.map f'.base).obj V = ⊤) (hV : ∀ b ∈ V, IsRegularLocalRing ↑(B.presheaf.stalk b)) :
    IsRegular Y'

    A scheme Y' covered by an open immersion ι from a regular scheme and by the inverse image of an open V over which f' : Y' ⟶ B is an isomorphism is regular as soon as B has regular local rings at the points of V and Y' is locally Noetherian.

    source
    instance TauCeti.AlgebraicGeometry.IsRegular.opens {X : AlgebraicGeometry.Scheme} [IsRegular X] (U : X.Opens) :
    IsRegular ↑U

    Every open subscheme of a regular scheme is regular.

    source
    theorem TauCeti.AlgebraicGeometry.isRegular_iff_openCover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
    IsRegular X ↔ ∀ (i : 𝒰.I₀), IsRegular (𝒰.X i)

    A scheme is regular if and only if all members of an open cover are regular.

    source
    instance TauCeti.AlgebraicGeometry.IsRegular.openCover {X : AlgebraicGeometry.Scheme} [IsRegular X] (𝒰 : X.OpenCover) (i : 𝒰.I₀) :
    IsRegular (𝒰.X i)

    The components of an open cover of a regular scheme are regular.

    source
    instance TauCeti.AlgebraicGeometry.isRegular_Spec (R : CommRingCat) [IsRegularRing ↑R] :
    IsRegular (AlgebraicGeometry.Spec R)

    The spectrum of a regular ring is regular.

    source
    theorem TauCeti.AlgebraicGeometry.isRegular_iff_forall_exists_affineOpens {X : AlgebraicGeometry.Scheme} :
    IsRegular X ↔ ∀ (point : ↥X), ∃ (openSet : ↑X.affineOpens), point ∈ ↑openSet ∧ IsRegularRing ↑(X.presheaf.obj (Opposite.op ↑openSet))

    A scheme is regular exactly when each point has an affine open neighbourhood with a regular ring of sections. This is Stacks, Definition 28.9.1 (02IS).

    source
    theorem TauCeti.AlgebraicGeometry.isRegular_iff_forall_affineOpens {X : AlgebraicGeometry.Scheme} :
    IsRegular X ↔ ∀ (U : ↑X.affineOpens), IsRegularRing ↑(X.presheaf.obj (Opposite.op ↑U))

    A scheme is regular exactly when its affine-open section rings are regular.

    source
    instance TauCeti.AlgebraicGeometry.IsRegular.component_regular {X : AlgebraicGeometry.Scheme} [IsRegular X] (U : ↑X.affineOpens) :
    IsRegularRing ↑(X.presheaf.obj (Opposite.op ↑U))

    The section ring of an affine open in a regular scheme is regular.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.isRegular_Spec_iff (R : CommRingCat) :
    IsRegular (AlgebraicGeometry.Spec R) ↔ IsRegularRing ↑R

    The spectrum of a ring is regular exactly when the ring is regular. This is the affine case of Stacks, Lemma 28.9.3 (02IU).

    source
    instance TauCeti.AlgebraicGeometry.IsRegular.isNormal {X : AlgebraicGeometry.Scheme} [IsRegular X] :
    IsNormalScheme X

    A regular scheme is normal. Stacks, Lemma 28.9.4 (0569).

    source
    theorem TauCeti.AlgebraicGeometry.IsRegular.of_isNormalScheme_of_topologicalKrullDim_le_one {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] [IsNormalScheme X] (hX : topologicalKrullDim ↥X ≤ 1) :
    IsRegular X

    A locally Noetherian normal scheme of dimension at most one is regular: each local ring is a Noetherian integrally closed local domain of dimension at most one, hence a field or a discrete valuation ring. Stacks, Lemma 10.119.7 (00PD).

    source
    theorem TauCeti.AlgebraicGeometry.IsRegular.uniqueFactorizationMonoid_stalk {X : AlgebraicGeometry.Scheme} [IsRegular X] (x : ↥X) (hx : Order.coheight x ≤ 2) :
    UniqueFactorizationMonoid ↑(X.presheaf.stalk x)

    Regular schemes are factorial in codimension at most two. The local ring of a regular scheme at a point of codimension at most two, such as any point of a regular model of a curve over a discrete valuation ring, is a unique factorization domain.