Documentation

TauCeti.AlgebraicGeometry.Curves.Node.Blowup

The branches of a nodal curve over a field #

Let X be a nodal curve over a field K, and let Sing(X/K) be its singular subscheme. The branch scheme of X is the scheme-theoretic inverse image of Sing(X/K) in the blowup Bl X of X along Sing(X/K),

E = Sing(X/K) ×_X Bl X.

This file proves that E ⟶ Sing(X/K) is finite étale of rank two: every node has exactly two branches, possibly conjugate over a separable quadratic extension of its residue field. No properness of X is needed. When X is proper, Sing(X/K) is moreover finite étale over K (AlgebraicGeometry.Scheme.isFinite_singularLocus_subschemeι_comp).

The proof is local at the nodes. A field-valued point t of Sing(X/K) factors through the local ring A of a standard syntomic affine chart of X at a prime containing the singular ideal. The singular ideal generates the maximal ideal 𝔪 of A, because the singular subscheme is unramified over K (Ideal.eq_maximalIdeal_of_formallyUnramified_quotient), and blowing up commutes with the flat base change to Spec A (TauCeti.AlgebraicGeometry.isPullback_affineBlowup_of_flat). The base change of Bl X to t is therefore the base change of the blowup of Spec A at its closed point. By Algebra.Presentation.exists_etale_tensor_affineBlowup_of_formallyUnramified, the maximal ideal is generated by x, y with y² ∈ x 𝔪, so that this blowup is the single chart Spec A[𝔪/x] (TauCeti.AlgebraicGeometry.isIso_affineBlowupι_of_sq_mem), whose closed fibre is an étale algebra of dimension two over the residue field. Thus the base change of E to every field-valued point of Sing(X/K) is finite étale of rank two. Since Sing(X/K) is étale over K, the morphism E ⟶ Sing(X/K) is étale, and it is finite since it is proper.

The points of E over a node are the tangent directions of the two branches through it. For a nodal curve over a field, the blowup along the singular subscheme is its normalization; that identification is not used here.

Main definitions #

Main results #

References #

source
noncomputable def AlgebraicGeometry.Scheme.branchScheme (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] :
Scheme

The branch scheme of a relative curve X over R: the scheme-theoretic inverse image Sing(X/R) ×_X Bl X of the singular subscheme Sing(X/R) in the blowup Bl X of X along Sing(X/R). For a nodal curve over a field it is finite étale of rank two over the singular subscheme (AlgebraicGeometry.Scheme.finrank_branchSchemeToSingularLocus): its points over a node are the tangent directions of the two branches through it.

Instances For
    source
    noncomputable def AlgebraicGeometry.Scheme.branchSchemeToSingularLocus (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] :
    branchScheme R X ⟶ (singularLocus R X).subscheme

    The projection of the branch scheme to the singular subscheme.

    Instances For
      source
      noncomputable def AlgebraicGeometry.Scheme.branchSchemeToBlowup (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] :
      branchScheme R X ⟶ (singularLocus R X).blowup

      The inclusion of the branch scheme into the blowup along the singular subscheme.

      Instances For
        source
        theorem AlgebraicGeometry.Scheme.branchSchemeToSingularLocus_subschemeι (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] :
        CategoryTheory.CategoryStruct.comp (branchSchemeToSingularLocus R X) (singularLocus R X).subschemeι = CategoryTheory.CategoryStruct.comp (branchSchemeToBlowup R X) (singularLocus R X).blowupToBase

        The two maps out of the branch scheme agree in X.

        source
        theorem AlgebraicGeometry.Scheme.branchSchemeToSingularLocus_subschemeι_assoc (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] {Z : Scheme} (h : X ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (branchSchemeToSingularLocus R X) (CategoryTheory.CategoryStruct.comp (singularLocus R X).subschemeι h) = CategoryTheory.CategoryStruct.comp (branchSchemeToBlowup R X) (CategoryTheory.CategoryStruct.comp (singularLocus R X).blowupToBase h)

        The two maps out of the branch scheme agree in X.

        source
        theorem AlgebraicGeometry.Scheme.isPullback_branchScheme (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] :
        CategoryTheory.IsPullback (branchSchemeToSingularLocus R X) (branchSchemeToBlowup R X) (singularLocus R X).subschemeι (singularLocus R X).blowupToBase

        The branch scheme is the inverse image of the singular subscheme in the blowup along it.

        source
        theorem AlgebraicGeometry.Scheme.exists_isPullback_branchSchemeToSingularLocus {R R' : Type u} [CommRing R] [CommRing R'] [Algebra R R'] [Module.Flat R R'] {X X' : Scheme} [X.Over (Spec ↧R)] [X'.Over (Spec ↧R')] {g : X' ⟶ X} [Flat (X ↘ Spec ↧R)] [LocallyOfFinitePresentation (X ↘ Spec ↧R)] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X ↘ Spec ↧R)] [Flat (X' ↘ Spec ↧R')] [LocallyOfFinitePresentation (X' ↘ Spec ↧R')] [TauCeti.AlgebraicGeometry.PureRelativeDimension 1 (X' ↘ Spec ↧R')] (H : CategoryTheory.IsPullback g (X' ↘ Spec ↧R') (X ↘ Spec ↧R) (Spec.map (CommRingCat.ofHom (algebraMap R R')))) :
        ∃ (f : branchScheme R' X' ⟶ branchScheme R X), CategoryTheory.IsPullback f (branchSchemeToSingularLocus R' X') (branchSchemeToSingularLocus R X) ((singularLocus R' X').subschemeMap (singularLocus R X) g ⋯)

        The branch scheme commutes with flat base change. If X' is the base change of X along a flat morphism Spec R' → Spec R, then the branch scheme of X' over its singular subscheme is the base change of the branch scheme of X along the morphism Sing(X'/R') ⟶ Sing(X/R) of singular subschemes (AlgebraicGeometry.Scheme.isPullback_singularLocus_subschemeι).

        source
        theorem AlgebraicGeometry.Scheme.etale_branchSchemeToSingularLocus {K : Type u} [Field K] (X : Scheme) [X.Over (Spec ↧K)] (hnodal : TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (X ↘ Spec ↧K)) :
        Etale (branchSchemeToSingularLocus K X)

        The branches of a nodal curve over a field are étale over its nodes. The branch scheme of a nodal curve over a field is étale over the singular subscheme.

        source
        theorem AlgebraicGeometry.Scheme.isFinite_branchSchemeToSingularLocus {K : Type u} [Field K] (X : Scheme) [X.Over (Spec ↧K)] (hnodal : TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (X ↘ Spec ↧K)) :
        IsFinite (branchSchemeToSingularLocus K X)

        The branches of a nodal curve over a field are finite over its nodes. The branch scheme of a nodal curve over a field is finite over the singular subscheme.

        source
        theorem AlgebraicGeometry.Scheme.finrank_branchSchemeToSingularLocus {K : Type u} [Field K] (X : Scheme) [X.Over (Spec ↧K)] (hnodal : TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (X ↘ Spec ↧K)) (s : ↥(singularLocus K X).subscheme) :
        Hom.finrank (branchSchemeToSingularLocus K X) s = 2

        Every node of a nodal curve over a field has two branches. The branch scheme of a nodal curve over a field has rank two over every point of the singular subscheme.