Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.TautologicalPoint

The tautological point of the projective Weierstrass model #

Let W be a Weierstrass curve over a commutative ring R. This file defines the tautological point [x : y : 1] of the projective Weierstrass model projModel W, with values in the affine coordinate ring R[W] = R[x, y] ⧸ (W(x, y)) (WeierstrassCurve.tautologicalPoint). The chart D₊(Z) of the projective model factors through it, and through the Laurent expansion R[W] → R⸨z⸩ at the point at infinity (WeierstrassCurve.laurentExpansion) it becomes the formal point [z : -1 : w(z)] along the zero section, with values in the power series ring R⟦z⟧.

Main definitions #

Main results #

References #

source
theorem WeierstrassCurve.equation_tautologicalPoint {R : Type u} [CommRing R] {W : WeierstrassCurve R} :
(W.toProjective.map (algebraMap R W.toAffine.CoordinateRing)).Equation ![(AdjoinRoot.of W.toAffine.polynomial) Polynomial.X, AdjoinRoot.root W.toAffine.polynomial, 1]

The coordinate functions (x, y, 1) over the affine coordinate ring R[W] solve the homogeneous Weierstrass equation of W.

source
noncomputable def WeierstrassCurve.tautologicalPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) :
AlgebraicGeometry.Spec ↧W.toAffine.CoordinateRing ⟶ W.projModel

The tautological point [x : y : 1] of the projective Weierstrass model, with values in the affine coordinate ring R[W] = R[x, y] ⧸ (W(x, y)). Rewrite with tautologicalPoint_def rather than unfolding this definition.

Instances For
    source
    theorem WeierstrassCurve.tautologicalPoint_def {R : Type u} [CommRing R] (W : WeierstrassCurve R) :
    W.tautologicalPoint = W.projModelPoint (algebraMap R W.toAffine.CoordinateRing) ⋯ ⋯

    The tautological point is the point of the projective model with homogeneous coordinates (x, y, 1), along algebraMap R R[W].

    source
    @[simp]
    theorem WeierstrassCurve.tautologicalPoint_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) :
    CategoryTheory.CategoryStruct.comp W.tautologicalPoint W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R W.toAffine.CoordinateRing))

    The tautological point lies over the morphism Spec R[W] ⟶ Spec R induced by algebraMap R R[W].

    source
    @[simp]
    theorem WeierstrassCurve.tautologicalPoint_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp W.tautologicalPoint (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R W.toAffine.CoordinateRing))) h

    The tautological point lies over the morphism Spec R[W] ⟶ Spec R induced by algebraMap R R[W].

    source
    theorem WeierstrassCurve.exists_SpecMap_comp_tautologicalPoint_eq_chartι {R : Type u} [CommRing R] (W : WeierstrassCurve R) :
    ∃ (k : W.toAffine.CoordinateRing →ₐ[R] W.toProjective.ChartRing 2), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom k.toRingHom)) W.tautologicalPoint = W.chartι 2

    The chart D₊(Z) of the projective model factors through the tautological point: the universal point of the chart is [X / Z : Y / Z : 1], the image of [x : y : 1] under an R-algebra map R[W] → ChartRing 2.

    source
    theorem WeierstrassCurve.SpecMap_laurentExpansion_tautologicalPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) :
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑W.laurentExpansion)) W.tautologicalPoint = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HahnSeries.ofPowerSeries ℤ R))) W.projModelFormalPoint

    The tautological point at infinity. Expanded in Laurent series at the point at infinity, the tautological point [x : y : 1] is the formal point [z : -1 : w(z)]: its coordinates are -y times those of the formal point.