Documentation

TauCeti.AlgebraicGeometry.Curves.Node.Relative

Nodal relative curves over an arbitrary base #

A morphism of schemes is at worst nodal of relative dimension one when this can be checked after restriction to affine opens of its target. On an affine base this agrees with the scheme-theoretic criterion: the morphism is syntomic of relative dimension one and its relative singular subscheme is unramified over the base.

The affine-local formulation makes nodality a morphism property. It is invariant under isomorphism, local on both source and target, stable under arbitrary base change, and contains smooth morphisms of relative dimension one. These are the closure properties needed to use nodal curves in families over nonaffine bases.

On an affine open U of a nodal relative curve over Spec R, the quotient of Γ(X, U) by the ideal of the singular locus is unramified over R (AlgebraicGeometry.Scheme.formallyUnramified_quotient_singularLocus_ideal).

References #

source
def TauCeti.AlgebraicGeometry.affineAtWorstNodalOfRelativeDimensionOne :
AlgebraicGeometry.AffineTargetMorphismProperty

The affine-target nodal-curve property. The existential presentation of the affine target by a spectrum makes the definition independent of the chosen affine presentation.

Instances For
    source
    instance TauCeti.AlgebraicGeometry.instRespectsIsoSchemeToPropertyAffineAtWorstNodalOfRelativeDimensionOne :
    affineAtWorstNodalOfRelativeDimensionOne.toProperty.RespectsIso
    source
    theorem TauCeti.AlgebraicGeometry.affineAtWorstNodalOfRelativeDimensionOne_iff_isoSpec {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) :
    affineAtWorstNodalOfRelativeDimensionOne f ↔ AffineAtWorstNodalOfRelativeDimensionOne (CategoryTheory.CategoryStruct.comp f Y.isoSpec.hom)

    On an affine target, the affine-target criterion can be tested using the canonical presentation by the spectrum of global sections.

    source
    theorem TauCeti.AlgebraicGeometry.affineAtWorstNodalOfRelativeDimensionOne_isStableUnderBaseChange :
    affineAtWorstNodalOfRelativeDimensionOne.IsStableUnderBaseChange

    The affine-target nodal criterion is stable under base change between affine bases.

    source
    instance TauCeti.AlgebraicGeometry.instIsLocalAffineAtWorstNodalOfRelativeDimensionOne :
    affineAtWorstNodalOfRelativeDimensionOne.IsLocal
    source
    def TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne :
    CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

    Being at worst nodal of relative dimension one is the affine-local extension of the scheme-theoretic criterion over spectra.

    Instances For
      source
      instance TauCeti.AlgebraicGeometry.instHasAffinePropertyAtWorstNodalOfRelativeDimensionOneAffineAtWorstNodalOfRelativeDimensionOne :
      AlgebraicGeometry.HasAffineProperty AtWorstNodalOfRelativeDimensionOne affineAtWorstNodalOfRelativeDimensionOne
      source
      theorem TauCeti.AlgebraicGeometry.atWorstNodalOfRelativeDimensionOne_iff_of_iso_spec {R : Type u} [CommRing R] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (e : Y ≅ AlgebraicGeometry.Spec ↧R) :
      AtWorstNodalOfRelativeDimensionOne f ↔ AffineAtWorstNodalOfRelativeDimensionOne (CategoryTheory.CategoryStruct.comp f e.hom)

      For a target isomorphic to a spectrum, the global nodal property is exactly the scheme-theoretic criterion after any chosen presentation of the target as a spectrum.

      source
      instance TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne.isStableUnderBaseChange :
      AtWorstNodalOfRelativeDimensionOne.IsStableUnderBaseChange

      Being at worst nodal of relative dimension one is stable under arbitrary base change.

      source
      instance TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne.isZariskiLocalAtSource :
      AlgebraicGeometry.IsZariskiLocalAtSource AtWorstNodalOfRelativeDimensionOne

      Being at worst nodal of relative dimension one is local on the source.

      source
      theorem TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne.syntomic {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (h : AtWorstNodalOfRelativeDimensionOne f) :
      SyntomicOfRelativeDimension 1 f

      A nodal relative curve is syntomic of relative dimension one.

      source
      theorem AlgebraicGeometry.Scheme.formallyUnramified_quotient_singularLocus_ideal {R : Type u} [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (hnodal : TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (X ↘ Spec ↧R)) (U : ↑X.affineOpens) :
      Algebra.FormallyUnramified R (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ (singularLocus R X).ideal U)

      Over an affine open U of a nodal relative curve over Spec R, the quotient of Γ(X, U) by the ideal of the singular locus is unramified over R: it is the ring of functions of the singular subscheme over U.

      source
      theorem TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne.of_smooth {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] :
      AtWorstNodalOfRelativeDimensionOne f

      A smooth morphism of relative dimension one is at worst nodal.

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

      The standard node chart is a nodal relative curve.