Module

CoordinateRing.lean

Nyll.SchemeTheory.PlaneCurves.CoordinateRing

30 declarations indexed from sourceView source ↗

Module documentation

Affine plane curves and their rational points

This file supplies the affine-coordinate-ring foundations used in Fried--Jarden, Section 6.2. A bivariate equation f defines the quotient of K[X, Y] by the principal ideal (f). A K-rational zero of f gives an evaluation map from this quotient to K; its kernel is the corresponding maximal ideal.

Imports4

Mathlib.Algebra.MvPolynomial.Eval
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Polynomial.UniqueFactorization
Mathlib.Tactic.Ring

Imported by6

abbrev

BivariatePolynomial

L33 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.BivariatePolynomial

Documentation

Bivariate polynomials, with coordinates indexed by 0 and 1.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open Function MvPolynomial
universe u

Lean source · statement

abbrev BivariatePolynomial (K : Type u) [CommSemiring K]

def

equationIdeal

L39 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.equationIdeal

Documentation

The principal ideal generated by an affine plane-curve equation.

Source context 7 commands

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

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

Lean source · statement

def equationIdeal (f : BivariatePolynomial K) :
    Ideal (BivariatePolynomial K)

abbrev

CoordinateRing

L44 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.CoordinateRing

Documentation

The affine coordinate ring K[X, Y] / (f).

Source context 7 commands

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

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

Lean source · statement

abbrev CoordinateRing (f : BivariatePolynomial K)

def

coordinate

L48 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.coordinate

Documentation

The image of a polynomial variable in the affine coordinate ring.

Source context 7 commands

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

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

Lean source · statement

def coordinate (f : BivariatePolynomial K) (i : Fin 2) : CoordinateRing f

def

coordinateX

L52 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.coordinateX

Documentation

The image of the first polynomial variable in the affine coordinate ring.

Source context 7 commands

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

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

Lean source · statement

def coordinateX (f : BivariatePolynomial K) : CoordinateRing f

def

coordinateY

L56 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.coordinateY

Documentation

The image of the second polynomial variable in the affine coordinate ring.

Source context 7 commands

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

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

Lean source · statement

def coordinateY (f : BivariatePolynomial K) : CoordinateRing f

theorem

quotient_mk_equation

L60 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.quotient_mk_equation

Source context 7 commands

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

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

Lean source · statement

theorem quotient_mk_equation
    (f : BivariatePolynomial K) :
    Ideal.Quotient.mk (equationIdeal f) f = 0

theorem

quotient_mk_C

L67 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.quotient_mk_C

Source context 7 commands

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

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

Lean source · statement

theorem quotient_mk_C
    (f : BivariatePolynomial K) (a : K) :
    Ideal.Quotient.mk (equationIdeal f) (MvPolynomial.C a) =
      algebraMap K (CoordinateRing f) a

structure

RationalPoint

L79 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.RationalPoint

Documentation

A K-rational point of the affine equation f: an actual pair of coordinates, indexed by Fin 2, at which f vanishes.

Source context 7 commands

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

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

Lean source · full declaration

structure RationalPoint (f : BivariatePolynomial K) where
  /-- The two coordinates of the rational point. -/
  coords : Fin 2 → K
  /-- The defining polynomial vanishes at these coordinates. -/
  isZero : MvPolynomial.aeval coords f = 0

def

polynomialEval

L86 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.polynomialEval

Documentation

Evaluation of bivariate polynomials at a rational point.

Source context 7 commands

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

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

Lean source · statement

def polynomialEval {f : BivariatePolynomial K} (p : RationalPoint f) :
    BivariatePolynomial K →ₐ[K] K

theorem

polynomialEval_X

L91 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.polynomialEval_X

Source context 7 commands

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

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

Lean source · statement

theorem polynomialEval_X
    {f : BivariatePolynomial K} (p : RationalPoint f) (i : Fin 2) :
    polynomialEval p (MvPolynomial.X i) = p.coords i

theorem

polynomialEval_surjective

L96 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.polynomialEval_surjective

Source context 7 commands

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

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

Lean source · statement

theorem polynomialEval_surjective
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    Function.Surjective (polynomialEval p)

theorem

polynomialEval_ker_isMaximal

L103 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.polynomialEval_ker_isMaximal

Source context 7 commands

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

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

Lean source · statement

theorem polynomialEval_ker_isMaximal
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    (RingHom.ker (polynomialEval p).toRingHom).IsMaximal

theorem

polynomialEval_ker_eq_span_coordinate_sub

L114 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.polynomialEval_ker_eq_span_coordinate_sub

Documentation

The kernel of evaluation is generated by the two translated coordinates X i - pᵢ. The proof is polynomial induction and does not use a Nullstellensatz.

Source context 7 commands

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

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

Lean source · full declaration

theorem polynomialEval_ker_eq_span_coordinate_sub
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    RingHom.ker (polynomialEval p).toRingHom =
      Ideal.span
        (Set.range fun i : Fin 2 =>
          MvPolynomial.X i - MvPolynomial.C (p.coords i)) := by
  let I : Ideal (BivariatePolynomial K) :=
    Ideal.span
      (Set.range fun i : Fin 2 =>
        MvPolynomial.X i - MvPolynomial.C (p.coords i))
  change RingHom.ker (polynomialEval p).toRingHom = I
  apply le_antisymm
  · intro g hg
    have hdiff :
        g - MvPolynomial.C (polynomialEval p g) ∈ I := by
      clear hg
      induction g using MvPolynomial.induction_on with
      | C a =>
          simp [polynomialEval]
      | add g h hg hh =>
          have hadd := I.add_mem hg hh
          convert hadd using 1
          simp only [map_add]
          ring
      | mul_X g i hg =>
          have hgenerator :
              MvPolynomial.X i -
                  MvPolynomial.C (p.coords i) ∈ I := by
            apply Ideal.subset_span
            exact Set.mem_range_self i
          have hmul :=
            I.add_mem
              (I.mul_mem_left (MvPolynomial.X i) hg)
              (I.mul_mem_left
                (MvPolynomial.C (polynomialEval p g)) hgenerator)
          convert hmul using 1
          simp only [map_mul, polynomialEval_X]
          ring
    rw [RingHom.mem_ker] at hg
    change polynomialEval p g = 0 at hg
    rw [hg] at hdiff
    simpa using hdiff
  · rw [Ideal.span_le]
    rintro g ⟨i, rfl⟩
    change
      MvPolynomial.X i - MvPolynomial.C (p.coords i) ∈
        RingHom.ker (polynomialEval p).toRingHom
    rw [RingHom.mem_ker]
    simp [polynomialEval]

theorem

equationIdeal_le_polynomialEval_ker

L168 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.equationIdeal_le_polynomialEval_ker

Documentation

The curve equation ideal lies in the kernel of evaluation at a rational point. This is the exact input needed to descend evaluation to the quotient.

Source context 7 commands

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

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

Lean source · statement

theorem equationIdeal_le_polynomialEval_ker
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    equationIdeal f ≤ RingHom.ker (polynomialEval p).toRingHom

def

pointEval

L175 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointEval

Documentation

Evaluation at a rational point, descended to the affine coordinate ring.

Source context 7 commands

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

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

Lean source · statement

def pointEval {f : BivariatePolynomial K} (p : RationalPoint f) :
    CoordinateRing f →ₐ[K] K

theorem

pointEval_mk

L182 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointEval_mk

Source context 7 commands

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

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

Lean source · statement

theorem pointEval_mk
    {f : BivariatePolynomial K} (p : RationalPoint f)
    (g : BivariatePolynomial K) :
    pointEval p (Ideal.Quotient.mk (equationIdeal f) g) =
      MvPolynomial.aeval p.coords g

theorem

pointEval_coordinateX

L190 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointEval_coordinateX

Source context 7 commands

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

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

Lean source · statement

theorem pointEval_coordinateX
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    pointEval p (coordinateX f) = p.coords 0

theorem

pointEval_coordinateY

L196 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointEval_coordinateY

Source context 7 commands

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

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

Lean source · statement

theorem pointEval_coordinateY
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    pointEval p (coordinateY f) = p.coords 1

theorem

pointEval_surjective

L201 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointEval_surjective

Source context 7 commands

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

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

Lean source · statement

theorem pointEval_surjective
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    Function.Surjective (pointEval p)

def

pointIdeal

L209 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointIdeal

Documentation

The maximal ideal of the affine coordinate ring associated to p.

Source context 7 commands

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

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

Lean source · statement

def pointIdeal {f : BivariatePolynomial K} (p : RationalPoint f) :
    Ideal (CoordinateRing f)

theorem

mem_pointIdeal_iff

L214 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.mem_pointIdeal_iff

Source context 7 commands

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

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

Lean source · statement

theorem mem_pointIdeal_iff
    {f : BivariatePolynomial K} (p : RationalPoint f)
    (z : CoordinateRing f) :
    z ∈ pointIdeal p ↔ pointEval p z = 0

theorem

pointIdeal_eq_map_polynomialEval_ker

L224 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointIdeal_eq_map_polynomialEval_ker

Documentation

The point ideal is the image in the coordinate ring of the polynomial evaluation kernel.

Source context 7 commands

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

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

Lean source · statement

theorem pointIdeal_eq_map_polynomialEval_ker
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    pointIdeal p =
      (RingHom.ker (polynomialEval p).toRingHom).map
        (Ideal.Quotient.mk (equationIdeal f))

theorem

pointIdeal_eq_span_coordinate_sub

L246 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointIdeal_eq_span_coordinate_sub

Documentation

Inside the affine coordinate ring, the point ideal is generated by the two coordinate differences x - p₀ and y - p₁.

Source context 7 commands

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

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

Lean source · full declaration

theorem pointIdeal_eq_span_coordinate_sub
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    pointIdeal p =
      Ideal.span
        (Set.range fun i : Fin 2 =>
          coordinate f i -
            algebraMap K (CoordinateRing f) (p.coords i)) := by
  rw [pointIdeal_eq_map_polynomialEval_ker,
    polynomialEval_ker_eq_span_coordinate_sub,
    Ideal.map_span]
  apply congrArg Ideal.span
  ext z
  constructor
  · rintro ⟨_, ⟨i, rfl⟩, rfl⟩
    exact ⟨i, by simp [coordinate]⟩
  · rintro ⟨i, rfl⟩
    refine
      ⟨MvPolynomial.X i - MvPolynomial.C (p.coords i),
        ⟨i, rfl⟩, ?_⟩
    simp [coordinate]

theorem

pointIdeal_isMaximal

L267 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointIdeal_isMaximal

Source context 7 commands

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

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

Lean source · statement

theorem pointIdeal_isMaximal
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    (pointIdeal p).IsMaximal

theorem

coordinateX_sub_mem_pointIdeal

L274 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.coordinateX_sub_mem_pointIdeal

Source context 7 commands

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

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

Lean source · statement

theorem coordinateX_sub_mem_pointIdeal
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    coordinateX f -
        algebraMap K (CoordinateRing f) (p.coords 0) ∈
      pointIdeal p

theorem

coordinateY_sub_mem_pointIdeal

L282 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.coordinateY_sub_mem_pointIdeal

Source context 7 commands

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

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

Lean source · statement

theorem coordinateY_sub_mem_pointIdeal
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    coordinateY f -
        algebraMap K (CoordinateRing f) (p.coords 1) ∈
      pointIdeal p

def

pointResidueEquiv

L291 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.pointResidueEquiv

Documentation

The residue algebra at a K-rational point is canonically K.

Source context 7 commands

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

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

Lean source · statement

def pointResidueEquiv
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    (CoordinateRing f ⧸ pointIdeal p) ≃ₐ[K] K

theorem

equationIdeal_isPrime

L304 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.equationIdeal_isPrime

Documentation

Irreducibility of the equation produces primality of its principal ideal. No domain conclusion is assumed as extra data.

Source context 7 commands

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

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

Lean source · statement

theorem equationIdeal_isPrime
    {f : BivariatePolynomial K} (hf : Irreducible f) :
    (equationIdeal f).IsPrime

theorem

coordinateRing_isDomain

L314 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.coordinateRing_isDomain

Documentation

The coordinate ring of an irreducible affine plane equation is a domain. This is derived from polynomial irreducibility via unique factorization.

Source context 7 commands

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

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

Lean source · statement

theorem coordinateRing_isDomain
    {f : BivariatePolynomial K} (hf : Irreducible f) :
    IsDomain (CoordinateRing f)

Module documentation

Affine plane curves and their rational points

Declarations