Documentation

TauCeti.AlgebraicGeometry.ProjectiveLine.Points

Distinguished points and sections of the projective line #

This file packages the zero and infinity sections and separates their closed points from the generic point. It is downstream of the affine-chart, smoothness, and integrality calculations.

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

The zero point as a section of the projective-line structure morphism.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.zeroSection_comp_structureMap (K : Type u) [Field K] :
    CategoryTheory.CategoryStruct.comp (zeroSection K) (structureMap K) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.zeroSection_closedPoint (K : Type u) [Field K] :
    (zeroSection K) (IsLocalRing.closedPoint K) = zeroPoint K

    The section zeroSection sends the unique point of Spec K to [0 : 1].

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

    The point at infinity as a section of the projective-line structure morphism.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.ProjectiveLine.infinitySection_comp_structureMap (K : Type u) [Field K] :
      CategoryTheory.CategoryStruct.comp (infinitySection K) (structureMap K) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.ProjectiveLine.infinitySection_closedPoint (K : Type u) [Field K] :
      (infinitySection K) (IsLocalRing.closedPoint K) = infinityPoint K

      The section infinitySection sends the unique point of Spec K to [1 : 0].

      source
      theorem TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPoint_ne_genericPoint (K : Type u) [Field K] :
      zeroPoint K ≠ genericPoint ↥(scheme K)

      The point [0 : 1] is not the generic point of the projective line.

      source
      theorem TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPoint_ne_genericPoint (K : Type u) [Field K] :
      infinityPoint K ≠ genericPoint ↥(scheme K)

      The point [1 : 0] is not the generic point of the projective line.