Documentation

TauCeti.AlgebraicGeometry.Curves.Node.Nodal

Nodal relative curves over an affine base #

A relative curve over Spec R is at worst nodal when it is syntomic of relative dimension one and its relative singular subscheme is unramified over Spec R. The singular subscheme is a closed subscheme and its structure morphism is locally of finite type, so this condition amounts to formal unramifiedness in the criterion.

The standard chart xy = a satisfies the criterion for every commutative ring and every smoothing parameter. In particular this includes the smooth charts where a is a unit.

Smooth relative curves satisfy the same criterion: their singular subscheme is empty.

Main result #

References #

source
def TauCeti.AlgebraicGeometry.AffineAtWorstNodalOfRelativeDimensionOne {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) :
Prop

The scheme-theoretic nodal-curve criterion over an affine base: the morphism is syntomic of relative dimension one, and its singular subscheme is unramified over the base.

Instances For
    source
    theorem TauCeti.AlgebraicGeometry.affineAtWorstNodalOfRelativeDimensionOne_iff {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} {f : X ⟶ AlgebraicGeometry.Spec ↧R} :
    AffineAtWorstNodalOfRelativeDimensionOne f ↔ ∃ (h : SyntomicOfRelativeDimension 1 f), Unramified (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R X).subschemeι f)

    A relative curve is at worst nodal exactly when it is syntomic of relative dimension one and its singular subscheme is unramified over the base.

    source
    theorem TauCeti.AlgebraicGeometry.AffineAtWorstNodalOfRelativeDimensionOne.mk {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} {f : X ⟶ AlgebraicGeometry.Spec ↧R} (hf : SyntomicOfRelativeDimension 1 f) (hs : Unramified (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R X).subschemeι f)) :
    AffineAtWorstNodalOfRelativeDimensionOne f

    Construct a nodal relative curve from syntomicity and unramifiedness of its singular subscheme.

    source
    theorem TauCeti.AlgebraicGeometry.AffineAtWorstNodalOfRelativeDimensionOne.syntomic {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} {f : X ⟶ AlgebraicGeometry.Spec ↧R} (h : AffineAtWorstNodalOfRelativeDimensionOne f) :
    SyntomicOfRelativeDimension 1 f

    A nodal relative curve is syntomic of relative dimension one.

    source
    theorem TauCeti.AlgebraicGeometry.AffineAtWorstNodalOfRelativeDimensionOne.unramified_singularLocus {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} {f : X ⟶ AlgebraicGeometry.Spec ↧R} (h : AffineAtWorstNodalOfRelativeDimensionOne f) :
    Unramified (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R X).subschemeι f)

    The singular subscheme of a nodal relative curve is unramified over the base.

    source
    theorem TauCeti.AlgebraicGeometry.AffineAtWorstNodalOfRelativeDimensionOne.of_isPullback {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} {R' : Type u} [CommRing R'] [Algebra R R'] [X.Over (AlgebraicGeometry.Spec ↧R)] {X' : AlgebraicGeometry.Scheme} [X'.Over (AlgebraicGeometry.Spec ↧R')] {g : X' ⟶ X} (H : CategoryTheory.IsPullback g (X' ↘ AlgebraicGeometry.Spec ↧R') (X ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R R')))) (h : AffineAtWorstNodalOfRelativeDimensionOne (X ↘ AlgebraicGeometry.Spec ↧R)) :
    AffineAtWorstNodalOfRelativeDimensionOne (X' ↘ AlgebraicGeometry.Spec ↧R')

    Nodal relative curves remain nodal after extension of the base ring.

    source
    theorem TauCeti.AlgebraicGeometry.AffineAtWorstNodalOfRelativeDimensionOne.of_smooth {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.SmoothOfRelativeDimension 1 (X ↘ AlgebraicGeometry.Spec ↧R)] :
    AffineAtWorstNodalOfRelativeDimensionOne (X ↘ AlgebraicGeometry.Spec ↧R)

    A smooth morphism of relative dimension one over an affine base is at worst nodal. Its relative singular subscheme is empty, so the singular-locus condition in the nodal criterion holds automatically.

    source
    theorem TauCeti.NodeAlgebra.affineAtWorstNodalOfRelativeDimensionOne {R : Type u} [CommRing R] (a : R) :
    AlgebraicGeometry.AffineAtWorstNodalOfRelativeDimensionOne (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R a))))

    The local model xy = a is a nodal relative curve over Spec R.