NYLL
Module

Dimension.lean

Nyll.SchemeTheory.PlaneCurves.Dimension
10 declarations indexed from sourceView source ↗

Module documentation

Dimension of an irreducible affine plane curve

This file derives the one-dimensionality needed in Fried--Jarden, Section 6.2, directly from an irreducible bivariate equation. The proof uses the correspondence between primes of a quotient and primes above its kernel, Krull's principal ideal theorem, and the Krull dimension of a polynomial ring in two variables over a field.

Imports5
Imported by3

Declarations

theorem

bivariatePolynomial_ringKrullDim

L34 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.bivariatePolynomial_ringKrullDim
Documentation

A polynomial ring in two variables over a field has Krull dimension two.

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 bivariatePolynomial_ringKrullDim :
    ringKrullDim (BivariatePolynomial K) = 2
theorem

equationIdeal_height_eq_one

L44 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.equationIdeal_height_eq_one
Documentation

The prime principal ideal of an irreducible plane equation has height one.

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 equationIdeal_height_eq_one
    {f : BivariatePolynomial K} (hf : Irreducible f) :
    (equationIdeal f).height = 1
theorem

coordinate_sub_irreducible

L54 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.coordinate_sub_irreducible
Documentation

A translated coordinate variable over a field is irreducible.

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 coordinate_sub_irreducible
    (i : Fin 2) (a : K) :
    Irreducible
      (MvPolynomial.X i - MvPolynomial.C a :
        BivariatePolynomial K)
theorem

pointIdeal_ne_bot

L73 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointIdeal_ne_bot
Documentation

The maximal ideal defined by a rational point of an irreducible affine plane curve is nonzero.

If it were zero, the polynomial evaluation kernel would equal (f). Thus f would divide both translated coordinate variables. Irreducibility would make those two variables associated, which is contradicted by evaluating one of them at zero and the other at one.

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 pointIdeal_ne_bot
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) :
    pointIdeal p ≠ ⊥
theorem

coordinateRing_dimensionLEOne

L135 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.coordinateRing_dimensionLEOne
Documentation

The coordinate ring of an irreducible affine plane equation has dimension at most one. No dimension hypothesis is supplied: it is derived from the height-one equation ideal inside the dimension-two polynomial 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 · statement
theorem coordinateRing_dimensionLEOne
    {f : BivariatePolynomial K} (hf : Irreducible f) :
    Ring.DimensionLEOne (CoordinateRing f)
theorem

atPrime_dimensionLEOne

L198 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.atPrime_dimensionLEOne
Documentation

Krull dimension at most one is preserved when the coordinate ring is localized at a prime ideal.

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 atPrime_dimensionLEOne
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : Ideal (CoordinateRing f)) [p.IsPrime] :
    Ring.DimensionLEOne (Localization.AtPrime p)
theorem

atPrime_nonzero_prime_eq_maximalIdeal

L213 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.atPrime_nonzero_prime_eq_maximalIdeal
Documentation

Every nonzero prime of a local ring of the irreducible curve is its maximal ideal.

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 atPrime_nonzero_prime_eq_maximalIdeal
    {f : BivariatePolynomial K} (hf : Irreducible f)
    {p : Ideal (CoordinateRing f)} [p.IsPrime]
    (P : Ideal (Localization.AtPrime p))
    (hP : P ≠ ⊥) (hPprime : P.IsPrime) :
    P = IsLocalRing.maximalIdeal (Localization.AtPrime p)
theorem

atPrime_existsUnique_nonzero_prime

L233 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.atPrime_existsUnique_nonzero_prime
Documentation

At a nonzero prime of the curve there is exactly one nonzero prime in the local 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 · statement
theorem atPrime_existsUnique_nonzero_prime
    {f : BivariatePolynomial K} (hf : Irreducible f)
    {p : Ideal (CoordinateRing f)} [p.IsPrime] (hp : p ≠ ⊥) :
    ∃! P : Ideal (Localization.AtPrime p), P ≠ ⊥ ∧ P.IsPrime
theorem

atPrime_isDiscreteValuationRing_of_isIntegrallyClosed

L259 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.atPrime_isDiscreteValuationRing_of_isIntegrallyClosed
Documentation

An integrally closed local ring at a nonzero maximal ideal of an irreducible affine plane curve is a discrete valuation 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
theorem atPrime_isDiscreteValuationRing_of_isIntegrallyClosed
    {f : BivariatePolynomial K} (hf : Irreducible f)
    {m : Ideal (CoordinateRing f)} [m.IsMaximal] (hm : m ≠ ⊥) :
    letI : m.IsPrime := (inferInstance : m.IsMaximal).isPrime
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    letI : IsDomain (Localization.AtPrime m) :=
      IsLocalization.isDomain_of_atPrime (Localization.AtPrime m) m
    IsIntegrallyClosed (Localization.AtPrime m) →
      IsDiscreteValuationRing (Localization.AtPrime m) := by
  intro hnormal
  let : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
  let : m.IsPrime := (inferInstance : m.IsMaximal).isPrime
  let : IsDomain (Localization.AtPrime m) :=
    IsLocalization.isDomain_of_atPrime (Localization.AtPrime m) m
  let : IsNoetherianRing (CoordinateRing f) := inferInstance
  let : IsNoetherianRing (Localization.AtPrime m) :=
    IsLocalization.isNoetherianRing m.primeCompl
      (Localization.AtPrime m) inferInstance
  let : IsLocalRing (Localization.AtPrime m) :=
    IsLocalization.AtPrime.isLocalRing (Localization.AtPrime m) m
  have hnotField :
      ¬ IsField (Localization.AtPrime m) :=
    IsLocalization.AtPrime.not_isField
      (CoordinateRing f) hm (Localization.AtPrime m)
  apply
    ((IsDiscreteValuationRing.TFAE
      (Localization.AtPrime m) hnotField).out 4 1).mp
  exact
    ⟨hnormal, atPrime_existsUnique_nonzero_prime hf hm⟩
theorem

pointLocalRing_isDiscreteValuationRing_of_isIntegrallyClosed

L293 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_isDiscreteValuationRing_of_isIntegrallyClosed
Documentation

The preceding DVR criterion specialized to the local ring of a rational 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 · full declaration
theorem pointLocalRing_isDiscreteValuationRing_of_isIntegrallyClosed
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) :
    letI : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    letI : IsDomain (Localization.AtPrime (pointIdeal p)) :=
      IsLocalization.isDomain_of_atPrime
        (Localization.AtPrime (pointIdeal p)) (pointIdeal p)
    IsIntegrallyClosed (Localization.AtPrime (pointIdeal p)) →
      IsDiscreteValuationRing
        (Localization.AtPrime (pointIdeal p)) := by
  intro hnormal
  let : (pointIdeal p).IsMaximal := pointIdeal_isMaximal p
  let : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
  exact
    atPrime_isDiscreteValuationRing_of_isIntegrallyClosed
      hf (pointIdeal_ne_bot hf p) hnormal

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.