Documentation

TauCeti.AlgebraicGeometry.ProjectiveLine.Basic

The projective line and its generic points #

This file realizes the projective line over a field K as the projective spectrum of the standard grading on K[X₀, X₁]. A field extension map K → F and an element g : F determine the F-valued point [g : 1].

For an integral curve with function field F, this is the generic-point morphism attached to a rational function. It is the first geometric input to the product formula in TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve".

source
@[reducible, inline]
abbrev TauCeti.AlgebraicGeometry.ProjectiveLine.homogeneousPieces (K : Type u) [Field K] (n : ℕ) :
Submodule K (MvPolynomial (Fin 2) K)

The standard grading of the homogeneous coordinate ring K[X₀, X₁].

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.AlgebraicGeometry.ProjectiveLine.instGradedAlgebraNatMvPolynomialFinOfNatHomogeneousPieces (K : Type u) [Field K] :
    GradedAlgebra (homogeneousPieces K)

    The standard graded-algebra structure on the homogeneous coordinate ring of the projective line. Mathlib intentionally does not install this instance globally because multivariate polynomials admit other weighted gradings.

    Equations
    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.AlgebraicGeometry.ProjectiveLine.scheme (K : Type u) [Field K] :
    AlgebraicGeometry.Scheme

    The projective line over K, realized as Proj K[X₀, X₁].

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev TauCeti.AlgebraicGeometry.ProjectiveLine.standardAffineOpen (K : Type u) [Field K] :
      (scheme K).Opens

      The standard affine chart D₊(X₁) of the projective line.

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.AlgebraicGeometry.ProjectiveLine.infinityAffineOpen (K : Type u) [Field K] :
        (scheme K).Opens

        The affine chart D₊(X₀) containing the point at infinity.

        Equations
        Instances For
          source
          theorem TauCeti.AlgebraicGeometry.ProjectiveLine.X_one_mem_degree_one (K : Type u) [Field K] :
          MvPolynomial.X 1 ∈ homogeneousPieces K 1
          source
          theorem TauCeti.AlgebraicGeometry.ProjectiveLine.X_zero_mem_degree_one (K : Type u) [Field K] :
          MvPolynomial.X 0 ∈ homogeneousPieces K 1
          source
          noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.affineCoordinateAway (K : Type u) [Field K] :
          HomogeneousLocalization.Away (homogeneousPieces K) (MvPolynomial.X 1)

          The degree-zero homogeneous fraction X₀ / X₁ on the standard affine chart.

          Equations
          Instances For
            source
            noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.affineCoordinate (K : Type u) [Field K] :
            ↑((scheme K).presheaf.obj (Opposite.op (standardAffineOpen K)))

            The regular function X₀ / X₁ on the standard affine chart D₊(X₁).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.inverseAffineCoordinateAway (K : Type u) [Field K] :
              HomogeneousLocalization.Away (homogeneousPieces K) (MvPolynomial.X 0)

              The degree-zero homogeneous fraction X₁ / X₀ on the affine chart containing infinity.

              Equations
              Instances For
                source
                noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.inverseAffineCoordinate (K : Type u) [Field K] :
                ↑((scheme K).presheaf.obj (Opposite.op (infinityAffineOpen K)))

                The regular function X₁ / X₀ on the affine chart D₊(X₀).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.degreeZeroRingEquiv (K : Type u) [Field K] :
                  K ≃+* ↥(homogeneousPieces K 0)

                  The constant-polynomial equivalence from K to the degree-zero part of K[X₀, X₁].

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.AlgebraicGeometry.ProjectiveLine.coe_degreeZeroRingEquiv_apply (K : Type u) [Field K] (r : K) :
                    ↑((degreeZeroRingEquiv K) r) = MvPolynomial.C r
                    source
                    noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                    AlgebraicGeometry.Spec (CommRingCat.of F) ⟶ scheme K

                    The F-valued point [g : 1] of the projective line associated to a field map K → F and an element g : F.

                    For a curve function field, this is the generic-point morphism defined by the corresponding rational function. The explicit field map makes the base-field structure part of the data and avoids choosing a global Algebra K F instance.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.ofInverseElement (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                      AlgebraicGeometry.Spec (CommRingCat.of F) ⟶ scheme K

                      The F-valued point [1 : g] of the projective line associated to a field map K → F and an element g : F.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[simp]
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofInverseElement_preimage_basicOpen_X_zero (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                        (TopologicalSpace.Opens.map (ofInverseElement K F ι g).base).obj (infinityAffineOpen K) = ⊤

                        The point [1 : g] lies in the affine chart D₊(X₀) containing infinity.

                        source
                        @[simp]
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement_preimage_basicOpen_X_one (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                        (TopologicalSpace.Opens.map (ofElement K F ι g).base).obj (AlgebraicGeometry.Proj.basicOpen (homogeneousPieces K) (MvPolynomial.X 1)) = ⊤

                        The point [g : 1] lies in the standard affine chart where the second homogeneous coordinate is nonzero.

                        source
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement_preimage_basicOpen_X_zero (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) (hg : g ≠ 0) :
                        (TopologicalSpace.Opens.map (ofElement K F ι g).base).obj (infinityAffineOpen K) = ⊤

                        If g is nonzero, the point [g : 1] also lies in the affine chart D₊(X₀) containing infinity.

                        source
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement_appLE_affineCoordinate (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (ofElement K F ι g) (standardAffineOpen K) ⊤ ⋯)) (affineCoordinate K) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of F)).inv) g

                        Pulling the standard affine coordinate X₀ / X₁ back along [g : 1] gives g.

                        This is the computational interface needed to distinguish the rational-function morphism of a non-global function from a constant morphism.

                        source
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofInverseElement_appLE_inverseAffineCoordinate (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (ofInverseElement K F ι g) (infinityAffineOpen K) ⊤ ⋯)) (inverseAffineCoordinate K) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of F)).inv) g

                        Pulling the inverse affine coordinate X₁ / X₀ back along [1 : g] gives g.

                        source
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement_appLE_inverseAffineCoordinate (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) (hg : g ≠ 0) :
                        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (ofElement K F ι g) (infinityAffineOpen K) ⊤ ⋯)) (inverseAffineCoordinate K) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of F)).inv) g⁻¹

                        Pulling the inverse affine coordinate X₁ / X₀ back along a nonzero point [g : 1] gives g⁻¹.

                        source
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofElement_toSpecZero (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                        CategoryTheory.CategoryStruct.comp (ofElement K F ι g) (AlgebraicGeometry.Proj.toSpecZero (homogeneousPieces K)) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (ι.comp (degreeZeroRingEquiv K).symm.toRingHom))

                        Before identifying the degree-zero homogeneous coordinate ring with K, the point [g : 1] lies over the field map from that degree-zero ring to F.

                        source
                        theorem TauCeti.AlgebraicGeometry.ProjectiveLine.ofInverseElement_toSpecZero (K F : Type u) [Field K] [Field F] (ι : K →+* F) (g : F) :
                        CategoryTheory.CategoryStruct.comp (ofInverseElement K F ι g) (AlgebraicGeometry.Proj.toSpecZero (homogeneousPieces K)) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (ι.comp (degreeZeroRingEquiv K).symm.toRingHom))

                        Before identifying the degree-zero homogeneous coordinate ring with K, the point [1 : g] lies over the field map from that degree-zero ring to F.