Documentation

TauCeti.AlgebraicGeometry.Curves.TwoChartModel.ProjectiveEmbedding

The two-chart model as a closed subscheme of a projective space #

Let F / k be an algebraic function field, let z ∈ Fˣ, and write D = (z)_∞ for its pole divisor. The two-chart model of F built from z is Proj of the section ring ⨁ₙ L(nD) (TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso). Suppose that every positive degree of this section ring is generated in degree one, that is, L(nD) ⊆ L(D)ⁿ for every n ≠ 0. Then the graded lift Sym_k L(D) → ⨁ₙ L(nD) of the identification of L(D) with the degree-one part is surjective in positive degrees, so Proj of the section ring is a closed subscheme of the projective space Proj (Sym_k L(D)) (AlgebraicGeometry.Proj.isClosedImmersion_map_gradedLift). Degree zero does not matter, which is why no exactness of the constants is needed here: L(0) is the full constant field of F. This file assembles these into a closed immersion of the two-chart model into Proj (Sym_k L(D)) over k: the embedding of the curve by the complete linear system of D. Since L(D) is finite-dimensional, Proj (Sym_k L(D)) is a projective space over k.

Generation in degree one is a genuine condition on z. It holds for every z when F has genus zero and k is the exact constant field of F (TauCeti.riemannRochSpace_nsmul_poles_le_pow_of_genus_eq_zero), for instance for the rational function field k(X); for z = X the space L(D) is spanned by 1 and X, so the target is the projective line. In every genus and over any constant field, it holds in positive degrees after replacing a transcendental z by a power z ^ e with e ≥ 1 and e ≥ 2g, where g is the genus of F over its full constant field (TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow_of_ne_zero), since the pole divisor of z ^ e is e D.

Since the two-chart model does not depend on the transcendental function it is built from (TauCeti.AlgebraicGeometry.twoChartModel.isoOfAlgEquiv), every two-chart model is projective: it is a closed subscheme over k of a projective space Proj (Sym_k V) with V finite-dimensional. Every regular proper curve over k is the two-chart model of its function field (AlgebraicGeometry.Scheme.isoTwoChartModel), so every regular proper curve is projective as well: it is projective over k in the sense of AlgebraicGeometry.Scheme.IsProjectiveOver.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.toProjSymmetricAlgebra {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hgen : ∀ (n : ℕ), n ≠ 0 → riemannRochSpace (n • Divisor.poles hF z) ≤ riemannRochSpace (Divisor.poles hF z) ^ n) :
twoChartModel hF ⋯ ⟶ AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k ↥(riemannRochSpace (Divisor.poles hF z)))

The embedding of the two-chart model by the sections of the pole divisor. If the section ring of D = (z)_∞ is generated in degree one in every positive degree, L(nD) ⊆ L(D)ⁿ for every n ≠ 0, the two-chart model built from z, identified with Proj of the section ring, maps to the projective space Proj (Sym_k L(D)) by the graded lift of the identification of L(D) with the degree-one part of the section ring.

Instances For
    source
    theorem TauCeti.AlgebraicGeometry.twoChartModel.toProjSymmetricAlgebra_def {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hgen : ∀ (n : ℕ), n ≠ 0 → riemannRochSpace (n • Divisor.poles hF z) ≤ riemannRochSpace (Divisor.poles hF z) ^ n) :
    toProjSymmetricAlgebra hF z hgen = CategoryTheory.CategoryStruct.comp (sectionRingProjIso hF z).inv (AlgebraicGeometry.Proj.map (SymmetricAlgebra.gradedLift k (Divisor.poles hF z).sectionRingGrade ↑(Divisor.poles hF z).sectionRingGradeOneEquiv) ⋯)

    The embedding by the sections of (z)_∞ is the inverse of the identification of the two-chart model with Proj of the section ring, followed by the morphism of projective spectra induced by the graded lift Sym_k L((z)_∞) → ⨁ₙ L(n (z)_∞).

    source
    instance TauCeti.AlgebraicGeometry.twoChartModel.isClosedImmersion_toProjSymmetricAlgebra {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hgen : ∀ (n : ℕ), n ≠ 0 → riemannRochSpace (n • Divisor.poles hF z) ≤ riemannRochSpace (Divisor.poles hF z) ^ n) :
    AlgebraicGeometry.IsClosedImmersion (toProjSymmetricAlgebra hF z hgen)

    The two-chart model is a closed subscheme of a projective space: when the section ring of (z)_∞ is generated in degree one in every positive degree, the embedding by the sections of (z)_∞ is a closed immersion.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.twoChartModel.toProjSymmetricAlgebra_projToSpec {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hgen : ∀ (n : ℕ), n ≠ 0 → riemannRochSpace (n • Divisor.poles hF z) ≤ riemannRochSpace (Divisor.poles hF z) ^ n) :
    CategoryTheory.CategoryStruct.comp (toProjSymmetricAlgebra hF z hgen) (SymmetricAlgebra.projToSpec k ↥(riemannRochSpace (Divisor.poles hF z))) = twoChartModel hF ⋯ ↘ AlgebraicGeometry.Spec ↧k

    The embedding by the sections of (z)_∞ lies over Spec k: followed by the coefficient morphism of the projective space, it is the structure morphism of the two-chart model.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.twoChartModel.toProjSymmetricAlgebra_projToSpec_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hgen : ∀ (n : ℕ), n ≠ 0 → riemannRochSpace (n • Divisor.poles hF z) ≤ riemannRochSpace (Divisor.poles hF z) ^ n) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧k ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (toProjSymmetricAlgebra hF z hgen) (CategoryTheory.CategoryStruct.comp (SymmetricAlgebra.projToSpec k ↥(riemannRochSpace (Divisor.poles hF z))) h) = CategoryTheory.CategoryStruct.comp (twoChartModel hF ⋯ ↘ AlgebraicGeometry.Spec ↧k) h

    The embedding by the sections of (z)_∞ lies over Spec k: followed by the coefficient morphism of the projective space, it is the structure morphism of the two-chart model.

    source
    instance TauCeti.AlgebraicGeometry.twoChartModel.instIsOverToProjSymmetricAlgebraSpecOf {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hgen : ∀ (n : ℕ), n ≠ 0 → riemannRochSpace (n • Divisor.poles hF z) ≤ riemannRochSpace (Divisor.poles hF z) ^ n) :
    AlgebraicGeometry.Scheme.Hom.IsOver (toProjSymmetricAlgebra hF z hgen) (AlgebraicGeometry.Spec ↧k)
    source
    theorem TauCeti.AlgebraicGeometry.twoChartModel.exists_isClosedImmersion_proj {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) :
    ∃ (V : Submodule k F) (_ : FiniteDimensional k ↥V) (f : twoChartModel hF ⋯ ⟶ AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k ↥V)), AlgebraicGeometry.IsClosedImmersion f ∧ AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧k)

    The two-chart model is projective. Over any field k, the two-chart model built from any transcendental x is a closed subscheme, over k, of the projective space Proj (Sym_k V) of a finite-dimensional k-vector space V.

    source
    instance AlgebraicGeometry.Scheme.isProjectiveOver_of_isCurveOver {k : Type u} [Field k] (X : Scheme) [X.Over (Spec ↧k)] [IsCurveOver k] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] :
    IsProjectiveOver k

    A regular proper curve is projective: if X is a curve over k whose codimension-one local rings are discrete valuation rings, then X is a closed subscheme, over k, of the projective space Proj (Sym_k V) of a finite-dimensional k-vector space V. No hypothesis on the constants of the function field k(X) is needed.