Documentation

TauCeti.AlgebraicGeometry.ProjectiveLine.Proper

The structure morphism of the projective line #

This file equips ProjectiveLine.scheme K with its structure morphism to Spec K. It identifies the degree-zero part of K[X₀, X₁] with K, verifies finite generation over that degree-zero part, and records that the structure morphism is locally of finite type and proper.

These are prerequisites for spreading a function-field point out to a rational map and then extending it on a proper regular curve, as required by the product formula in TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve".

source
instance TauCeti.AlgebraicGeometry.ProjectiveLine.instFiniteTypeSubtypeMvPolynomialFinOfNatNatMemSubmoduleHomogeneousPieces (K : Type u) [Field K] :
Algebra.FiniteType (↥(homogeneousPieces K 0)) (MvPolynomial (Fin 2) K)

The homogeneous coordinate ring of the projective line is finitely generated over its degree-zero part.

source
noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.structureMap (K : Type u) [Field K] :
scheme K ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)

The structure morphism ℙ¹_K ⟶ Spec K.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement_comp_structureMap (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
    CategoryTheory.CategoryStruct.comp (ofElement K F ι g) (structureMap K) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ι)

    The point [g : 1] lies over the base-field map K → F.

    source
    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement_comp_structureMap_assoc (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (ofElement K F ι g) (CategoryTheory.CategoryStruct.comp (structureMap K) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ι)) h

    The point [g : 1] lies over the base-field map K → F.

    source
    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofInverseElement_comp_structureMap (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
    CategoryTheory.CategoryStruct.comp (ofInverseElement K F ι g) (structureMap K) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ι)

    The point [1 : g] lies over the base-field map K → F.

    source
    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofInverseElement_comp_structureMap_assoc (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (ofInverseElement K F ι g) (CategoryTheory.CategoryStruct.comp (structureMap K) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ι)) h

    The point [1 : g] lies over the base-field map K → F.

    source
    instance TauCeti.AlgebraicGeometry.ProjectiveLine.instLocallyOfFiniteTypeStructureMap (K : Type u) [Field K] :
    AlgebraicGeometry.LocallyOfFiniteType (structureMap K)
    source
    instance TauCeti.AlgebraicGeometry.ProjectiveLine.instIsProperStructureMap (K : Type u) [Field K] :
    AlgebraicGeometry.IsProper (structureMap K)
    source
    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.structureMap_valuativeCriterion (K : Type u) [Field K] :
    AlgebraicGeometry.ValuativeCriterion (structureMap K)

    The structure morphism of the projective line satisfies the valuative criterion.