Module

RationalPoints.lean

Nyll.SchemeTheory.PlaneCurves.RationalPoints

6 declarations indexed from sourceView source ↗

Module documentation

Rational points from coordinate-ring morphisms

Every K-algebra map from an affine plane-curve coordinate ring to K comes from a unique rational point. Consequently, coordinate-ring equivalences transport rational points and their maximal ideals.

Imports1

Nyll.SchemeTheory.PlaneCurves.CoordinateRing

Imported by2

def

ofAlgHom

L28 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.RationalPoint.ofAlgHom

Documentation

Recover a rational point from a K-algebra map of its coordinate ring.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
universe u
variable {K : Type u} [Field K]

Lean source · full declaration

def RationalPoint.ofAlgHom
    {f : BivariatePolynomial K}
    (φ : CoordinateRing f →ₐ[K] K) :
    RationalPoint f where
  coords i := φ (coordinate f i)
  isZero := by
    have hcomp :
        MvPolynomial.aeval (fun i => φ (coordinate f i)) =
          φ.comp (Ideal.Quotient.mkₐ K (equationIdeal f)) := by
      apply MvPolynomial.algHom_ext
      intro i
      simp [coordinate]
    rw [hcomp]
    have hfzero :
        Ideal.Quotient.mk (equationIdeal f) f = 0 := by
      rw [Ideal.Quotient.eq_zero_iff_mem]
      exact Ideal.subset_span (Set.mem_singleton f)
    change φ (Ideal.Quotient.mk (equationIdeal f) f) = 0
    rw [hfzero, map_zero]

theorem

ofAlgHom_coords

L49 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.RationalPoint.ofAlgHom_coords

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
universe u
variable {K : Type u} [Field K]

Lean source · statement

theorem RationalPoint.ofAlgHom_coords
    {f : BivariatePolynomial K}
    (φ : CoordinateRing f →ₐ[K] K) (i : Fin 2) :
    (RationalPoint.ofAlgHom φ).coords i = φ (coordinate f i)

theorem

pointEval_ofAlgHom

L57 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointEval_ofAlgHom

Documentation

Evaluation at the recovered point is the original algebra map.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
universe u
variable {K : Type u} [Field K]

Lean source · statement

theorem pointEval_ofAlgHom
    {f : BivariatePolynomial K}
    (φ : CoordinateRing f →ₐ[K] K) :
    pointEval (RationalPoint.ofAlgHom φ) = φ

def

mapCoordinateRingEquiv

L67 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.RationalPoint.mapCoordinateRingEquiv

Documentation

Transport a rational point contravariantly along a coordinate-ring equivalence.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
universe u
variable {K : Type u} [Field K]

Lean source · statement

def RationalPoint.mapCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f) :
    RationalPoint g

theorem

pointEval_mapCoordinateRingEquiv

L76 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointEval_mapCoordinateRingEquiv

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
universe u
variable {K : Type u} [Field K]

Lean source · statement

theorem pointEval_mapCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f) :
    pointEval (p.mapCoordinateRingEquiv e) =
      (pointEval p).comp e.symm.toAlgHom

theorem

map_pointIdeal_mapCoordinateRingEquiv

L85 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.map_pointIdeal_mapCoordinateRingEquiv

Documentation

The point ideal is carried to the point ideal of the transported point.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
universe u
variable {K : Type u} [Field K]

Lean source · statement

theorem map_pointIdeal_mapCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f) :
    (pointIdeal p).map e.toRingEquiv.toRingHom =
      pointIdeal (p.mapCoordinateRingEquiv e)

Module documentation

Rational points from coordinate-ring morphisms

Declarations

ofAlgHom

ofAlgHom_coords

pointEval_ofAlgHom

mapCoordinateRingEquiv

pointEval_mapCoordinateRingEquiv

map_pointIdeal_mapCoordinateRingEquiv