Documentation

TauCeti.AlgebraicGeometry.Curves.ProjectiveLine

The projective line is the two-chart model of k(X) #

The projective line ℙ¹_k = Proj k[X₀, X₁] over a field k (TauCeti.AlgebraicGeometry.projectiveLine) is a regular proper curve over k whose function field is the rational function field k(X), the function X₁ / X₀ going to X (TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv). By the classification of regular proper curves (AlgebraicGeometry.Scheme.isoTwoChartModel), it is therefore isomorphic over k to the two-chart model of k(X) built from X, the scheme glued from Spec k[X] and Spec k[X⁻¹].

For a function field F finite over k(X), the two-chart model of F built from the image x of X maps finitely to the two-chart model of k(X) (TauCeti.AlgebraicGeometry.twoChartModel.isFinite_map), and is the normalization of the latter in F (TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso). Composing with the isomorphism above gives the projection ν_F of the two-chart model of F onto ℙ¹_k itself: a finite morphism over k whose pullback of rational functions is the inclusion k(X) → F.

Main definitions #

Main results #

References #

The projective line is a regular proper curve #

source
instance TauCeti.AlgebraicGeometry.projectiveLine.isCurveOver (k : Type u) [Field k] :
AlgebraicGeometry.Scheme.IsCurveOver k

The projective line is a curve over k: it is integral and proper over k, and its dimension is the transcendence degree one of its function field k(X).

The projective line is the two-chart model of k(X) #

source
noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.isoTwoChartModel (k : Type u) [Field k] :
projectiveLine k ≅ twoChartModel ⋯ ⋯

The projective line is the two-chart model of k(X): the isomorphism over k of ℙ¹_k = Proj k[X₀, X₁] with the scheme glued from Spec k[X] and Spec k[X⁻¹], whose pullback of rational functions is the identity of k(X) (functionFieldEquiv_functionFieldMap_isoTwoChartModel_hom).

Instances For
    source
    instance TauCeti.AlgebraicGeometry.projectiveLine.instIsOverHomSchemeIsoTwoChartModelSpecOf (k : Type u) [Field k] :
    AlgebraicGeometry.Scheme.Hom.IsOver (isoTwoChartModel k).hom (AlgebraicGeometry.Spec ↧k)

    The isomorphism ℙ¹_k ⟶ twoChartModel is a morphism over k.

    source
    instance TauCeti.AlgebraicGeometry.projectiveLine.instIsOverInvSchemeIsoTwoChartModelSpecOf (k : Type u) [Field k] :
    AlgebraicGeometry.Scheme.Hom.IsOver (isoTwoChartModel k).inv (AlgebraicGeometry.Spec ↧k)

    The isomorphism twoChartModel ⟶ ℙ¹_k is a morphism over k.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv_functionFieldMap_isoTwoChartModel_hom (k : Type u) [Field k] (z : RatFunc k) :
    (functionFieldEquiv k) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.functionFieldMap (isoTwoChartModel k).hom)) ((twoChartModel.functionFieldEquiv ⋯).symm z)) = z

    The pullback of rational functions along ℙ¹_k ≅ twoChartModel is the identity of k(X): under the identifications of both function fields with k(X), the pullback along the isomorphism ℙ¹_k ⟶ twoChartModel fixes every rational function.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv_functionFieldMap_isoTwoChartModel_inv (k : Type u) [Field k] (z : RatFunc k) :
    (twoChartModel.functionFieldEquiv ⋯) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.functionFieldMap (isoTwoChartModel k).inv)) ((functionFieldEquiv k).symm z)) = z

    The pullback of rational functions along the isomorphism twoChartModel ⟶ ℙ¹_k is the identity of k(X), under the identifications of both function fields with k(X).

    The projection of a two-chart model to the projective line #

    source
    noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.toProjectiveLine {k F : Type u} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F] (hF : IsFunctionField k F) (hx : (algebraMap (RatFunc k) F) RatFunc.X ≠ 0) :
    twoChartModel hF hx ⟶ projectiveLine k

    The projection ν_F of the two-chart model of F to the projective line, for a function field F integral, equivalently finite, over k(X): the morphism from the two-chart model of F built from the image x of X to ℙ¹_k, glued from Spec of the inclusions k[X] → 𝒪_x and k[X⁻¹] → 𝒪_{x⁻¹} and read through the isomorphism of ℙ¹_k with the two-chart model of k(X).

    Instances For
      source
      instance TauCeti.AlgebraicGeometry.twoChartModel.instIsOverToProjectiveLineSpecOf {k F : Type u} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F] (hF : IsFunctionField k F) (hx : (algebraMap (RatFunc k) F) RatFunc.X ≠ 0) :
      AlgebraicGeometry.Scheme.Hom.IsOver (toProjectiveLine hF hx) (AlgebraicGeometry.Spec ↧k)

      The projection to the projective line is a morphism over k.

      source
      instance TauCeti.AlgebraicGeometry.twoChartModel.instIsDominantToProjectiveLine {k F : Type u} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F] (hF : IsFunctionField k F) (hx : (algebraMap (RatFunc k) F) RatFunc.X ≠ 0) :
      AlgebraicGeometry.IsDominant (toProjectiveLine hF hx)

      The projection to the projective line is dominant.

      source
      instance TauCeti.AlgebraicGeometry.twoChartModel.isFinite_toProjectiveLine {k F : Type u} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F] (hF : IsFunctionField k F) (hx : (algebraMap (RatFunc k) F) RatFunc.X ≠ 0) :
      AlgebraicGeometry.IsFinite (toProjectiveLine hF hx)

      The projection of the two-chart model of F to the projective line is finite. This includes inseparable extensions F / k(X).

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv_functionFieldMap_toProjectiveLine {k F : Type u} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F] (hF : IsFunctionField k F) (hx : (algebraMap (RatFunc k) F) RatFunc.X ≠ 0) (z : RatFunc k) :
      (functionFieldEquiv ⋯) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.functionFieldMap (toProjectiveLine hF hx))) ((projectiveLine.functionFieldEquiv k).symm z)) = (algebraMap (RatFunc k) F) z

      The pullback of rational functions along the projection to the projective line is the inclusion k(X) → F, under the identifications of the function fields of ℙ¹_k and of the two-chart model of F with k(X) and F.