NYLL
Module

SimpleImpliesNormal.lean

Nyll.SchemeTheory.PlaneCurves.SimpleImpliesNormal
13 declarations indexed from sourceView source ↗

Module documentation

Simple points of affine plane curves

This file proves the simple-to-normal direction of Fried--Jarden, Lemma 6.2.3. At a point where one partial derivative is nonzero, the first-order decomposition of the curve equation eliminates the corresponding translated coordinate in the point localization. Thus its maximal ideal is generated by the other translated coordinate, so the local ring is a discrete valuation ring and in particular is normal.

Imports5
Imported by1

Declarations

def

pointLocalRingCommRing

L42 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRingCommRing
Documentation

The canonical commutative-ring structure on a point localization. The two coordinate calculations below share this source instead of separately running synthesis through the quotient and localization abbreviations.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · statement
def pointLocalRingCommRing
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    CommRing (PointLocalRing p)
theorem

pointLocalRing_maximalIdeal_eq_span_coordinateY_sub_of_partialAt_zero_ne

L51 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_maximalIdeal_eq_span_coordinateY_sub_of_partialAt_zero_ne
Documentation

If the X-partial derivative is nonzero at p, the maximal ideal of the point local ring is generated by the image of y - p_y.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem pointLocalRing_maximalIdeal_eq_span_coordinateY_sub_of_partialAt_zero_ne
    {f : BivariatePolynomial K} (p : RationalPoint f)
    (hpartial : partialAt p 0 ≠ 0) :
    maximalIdeal (PointLocalRing p) =
      Ideal.span
        {algebraMap (CoordinateRing f) (PointLocalRing p)
          (coordinateY f -
            algebraMap K (CoordinateRing f) (p.coords 1))}
theorem

pointLocalRing_maximalIdeal_eq_span_coordinateX_sub_of_partialAt_one_ne

L158 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_maximalIdeal_eq_span_coordinateX_sub_of_partialAt_one_ne
Documentation

If the Y-partial derivative is nonzero at p, the maximal ideal of the point local ring is generated by the image of x - p_x.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem pointLocalRing_maximalIdeal_eq_span_coordinateX_sub_of_partialAt_one_ne
    {f : BivariatePolynomial K} (p : RationalPoint f)
    (hpartial : partialAt p 1 ≠ 0) :
    maximalIdeal (PointLocalRing p) =
      Ideal.span
        {algebraMap (CoordinateRing f) (PointLocalRing p)
          (coordinateX f -
            algebraMap K (CoordinateRing f) (p.coords 0))}
theorem

pointLocalRing_isDiscreteValuationRing_of_maximalIdeal_eq_span

L267 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_isDiscreteValuationRing_of_maximalIdeal_eq_span
Documentation

The regularity step used by both coordinate directions. Once a generator of the maximal ideal is supplied, the point-localization and Noetherian instances are produced once here, rather than reconstructed independently in the two partial-derivative theorems.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
theorem pointLocalRing_isDiscreteValuationRing_of_maximalIdeal_eq_span
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (parameter : PointLocalRing p)
    (hspan :
      maximalIdeal (PointLocalRing p) = Ideal.span {parameter}) :
    letI : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    letI : IsDomain (PointLocalRing p) :=
      IsLocalization.isDomain_of_atPrime
        (PointLocalRing p) (pointIdeal p)
    IsDiscreteValuationRing (PointLocalRing p) := by
  let : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
  let : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
  let : IsDomain (PointLocalRing p) :=
    IsLocalization.isDomain_of_atPrime
      (PointLocalRing p) (pointIdeal p)
  let : IsNoetherianRing (CoordinateRing f) := inferInstance
  let : IsNoetherianRing (PointLocalRing p) :=
    IsLocalization.isNoetherianRing (pointIdeal p).primeCompl
      (PointLocalRing p) inferInstance
  have hnotField : ¬ IsField (PointLocalRing p) :=
    IsLocalization.AtPrime.not_isField
      (CoordinateRing f) (pointIdeal_ne_bot hf p) (PointLocalRing p)
  apply
    ((IsDiscreteValuationRing.TFAE
      (PointLocalRing p) hnotField).out 5 1).mp
  exact ⟨parameter, hspan⟩
theorem

pointLocalRing_isDiscreteValuationRing_of_partialAt_zero_ne

L299 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_isDiscreteValuationRing_of_partialAt_zero_ne
Documentation

Nonvanishing of the X-partial derivative makes the point local ring a discrete valuation ring.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
theorem pointLocalRing_isDiscreteValuationRing_of_partialAt_zero_ne
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hpartial : partialAt p 0 ≠ 0) :
    letI : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    letI : IsDomain (PointLocalRing p) :=
      IsLocalization.isDomain_of_atPrime
        (PointLocalRing p) (pointIdeal p)
    IsDiscreteValuationRing (PointLocalRing p) := by
  apply
    pointLocalRing_isDiscreteValuationRing_of_maximalIdeal_eq_span
      hf p
        (algebraMap (CoordinateRing f) (PointLocalRing p)
          (coordinateY f -
            algebraMap K (CoordinateRing f) (p.coords 1)))
  exact
    pointLocalRing_maximalIdeal_eq_span_coordinateY_sub_of_partialAt_zero_ne
      p hpartial
theorem

pointLocalRing_isDiscreteValuationRing_of_partialAt_one_ne

L322 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_isDiscreteValuationRing_of_partialAt_one_ne
Documentation

Nonvanishing of the Y-partial derivative makes the point local ring a discrete valuation ring.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
theorem pointLocalRing_isDiscreteValuationRing_of_partialAt_one_ne
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hpartial : partialAt p 1 ≠ 0) :
    letI : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    letI : IsDomain (PointLocalRing p) :=
      IsLocalization.isDomain_of_atPrime
        (PointLocalRing p) (pointIdeal p)
    IsDiscreteValuationRing (PointLocalRing p) := by
  apply
    pointLocalRing_isDiscreteValuationRing_of_maximalIdeal_eq_span
      hf p
        (algebraMap (CoordinateRing f) (PointLocalRing p)
          (coordinateX f -
            algebraMap K (CoordinateRing f) (p.coords 0)))
  exact
    pointLocalRing_maximalIdeal_eq_span_coordinateX_sub_of_partialAt_one_ne
      p hpartial
theorem

pointLocalRing_canonicalValuation_coordinateY_sub_eq_exp_neg_one

L346 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_canonicalValuation_coordinateY_sub_eq_exp_neg_one
Documentation

In mathlib's multiplicative normalization, the canonical valuation sends the local parameter y - p_y to exp (-1). Equivalently, its additive order is one, as in the final assertion of Fried--Jarden, Lemma 6.2.3.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
theorem pointLocalRing_canonicalValuation_coordinateY_sub_eq_exp_neg_one
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hpartial : partialAt p 0 ≠ 0) :
    letI : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    letI : IsDomain (PointLocalRing p) :=
      IsLocalization.isDomain_of_atPrime
        (PointLocalRing p) (pointIdeal p)
    letI : IsDiscreteValuationRing (PointLocalRing p) :=
      pointLocalRing_isDiscreteValuationRing_of_partialAt_zero_ne
        hf p hpartial
    (IsDiscreteValuationRing.maximalIdeal
        (PointLocalRing p)).valuation (CoordinateFunctionField f)
      (algebraMap (PointLocalRing p) (CoordinateFunctionField f)
        (algebraMap (CoordinateRing f) (PointLocalRing p)
          (coordinateY f -
            algebraMap K (CoordinateRing f) (p.coords 1)))) =
      WithZero.exp (-1 : ℤ) := by
  let : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
  let : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
  let : IsDomain (PointLocalRing p) :=
    IsLocalization.isDomain_of_atPrime
      (PointLocalRing p) (pointIdeal p)
  let : IsDiscreteValuationRing (PointLocalRing p) :=
    pointLocalRing_isDiscreteValuationRing_of_partialAt_zero_ne
      hf p hpartial
  let parameter : PointLocalRing p :=
    algebraMap (CoordinateRing f) (PointLocalRing p)
      (coordinateY f -
        algebraMap K (CoordinateRing f) (p.coords 1))
  have hspan :
      maximalIdeal (PointLocalRing p) = Ideal.span {parameter} := by
    exact
      pointLocalRing_maximalIdeal_eq_span_coordinateY_sub_of_partialAt_zero_ne
        p hpartial
  have hparameter_ne : parameter ≠ 0 := by
    intro hzero
    apply IsDiscreteValuationRing.not_a_field (PointLocalRing p)
    simpa [hzero] using hspan
  change
    (IsDiscreteValuationRing.maximalIdeal
        (PointLocalRing p)).valuation (CoordinateFunctionField f)
      (algebraMap (PointLocalRing p) (CoordinateFunctionField f)
        parameter) =
      WithZero.exp (-1 : ℤ)
  rw [IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap]
  exact
    (IsDiscreteValuationRing.maximalIdeal
      (PointLocalRing p)).intValuation_singleton
        hparameter_ne (by
          simpa [IsDiscreteValuationRing.maximalIdeal] using hspan)
theorem

pointLocalRing_ordFrac_coordinateY_sub_eq_exp_one

L402 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.pointLocalRing_ordFrac_coordinateY_sub_eq_exp_one
Documentation

The additive normalization of the same statement: the order of vanishing of y - p_y is one.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
theorem pointLocalRing_ordFrac_coordinateY_sub_eq_exp_one
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hpartial : partialAt p 0 ≠ 0) :
    letI : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    letI : IsDomain (PointLocalRing p) :=
      IsLocalization.isDomain_of_atPrime
        (PointLocalRing p) (pointIdeal p)
    letI : IsDiscreteValuationRing (PointLocalRing p) :=
      pointLocalRing_isDiscreteValuationRing_of_partialAt_zero_ne
        hf p hpartial
    Ring.ordFrac (PointLocalRing p)
      (algebraMap (PointLocalRing p) (CoordinateFunctionField f)
        (algebraMap (CoordinateRing f) (PointLocalRing p)
          (coordinateY f -
            algebraMap K (CoordinateRing f) (p.coords 1)))) =
      WithZero.exp (1 : ℤ) := by
  let : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
  let : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
  let : IsDomain (PointLocalRing p) :=
    IsLocalization.isDomain_of_atPrime
      (PointLocalRing p) (pointIdeal p)
  let : IsDiscreteValuationRing (PointLocalRing p) :=
    pointLocalRing_isDiscreteValuationRing_of_partialAt_zero_ne
      hf p hpartial
  let parameter : PointLocalRing p :=
    algebraMap (CoordinateRing f) (PointLocalRing p)
      (coordinateY f -
        algebraMap K (CoordinateRing f) (p.coords 1))
  have hspan :
      maximalIdeal (PointLocalRing p) = Ideal.span {parameter} := by
    exact
      pointLocalRing_maximalIdeal_eq_span_coordinateY_sub_of_partialAt_zero_ne
        p hpartial
  have hirreducible : Irreducible parameter :=
    (IsDiscreteValuationRing.irreducible_iff_uniformizer parameter).mpr
      hspan
  change
    Ring.ordFrac (PointLocalRing p)
      (algebraMap (PointLocalRing p) (CoordinateFunctionField f)
        parameter) =
      WithZero.exp (1 : ℤ)
  exact Ring.ordFrac_irreducible hirreducible
theorem

isNormalAt_of_pointLocalRing_isDiscreteValuationRing

L451 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.isNormalAt_of_pointLocalRing_isDiscreteValuationRing
Documentation

A point-local DVR is normal. This is the single bridge which installs the canonical point-localization domain and regularity instances before asking for integral closedness.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
theorem isNormalAt_of_pointLocalRing_isDiscreteValuationRing
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f)
    (hDVR :
      letI : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
      letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
      letI : IsDomain (PointLocalRing p) :=
        IsLocalization.isDomain_of_atPrime
          (PointLocalRing p) (pointIdeal p)
      IsDiscreteValuationRing (PointLocalRing p)) :
    IsNormalAt p := by
  let : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
  let : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
  let : IsDomain (PointLocalRing p) :=
    IsLocalization.isDomain_of_atPrime
      (PointLocalRing p) (pointIdeal p)
  let : IsDiscreteValuationRing (PointLocalRing p) := hDVR
  change IsIntegrallyClosed (PointLocalRing p)
  infer_instance
theorem

isNormalAt_of_partialAt_zero_ne

L472 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.isNormalAt_of_partialAt_zero_ne
Documentation

A nonzero X-partial derivative makes the point normal.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem isNormalAt_of_partialAt_zero_ne
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hpartial : partialAt p 0 ≠ 0) :
    IsNormalAt p
theorem

isNormalAt_of_partialAt_one_ne

L482 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.isNormalAt_of_partialAt_one_ne
Documentation

A nonzero Y-partial derivative makes the point normal.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem isNormalAt_of_partialAt_one_ne
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hpartial : partialAt p 1 ≠ 0) :
    IsNormalAt p
theorem

isNormalAt_of_isSimple

L495 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.isNormalAt_of_isSimple
Documentation

Fried--Jarden, Lemma 6.2.3, simple-to-normal direction: every simple rational point of an irreducible affine plane curve is normal.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem isNormalAt_of_isSimple
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hsimple : IsSimple p) :
    IsNormalAt p
theorem

isNormalAt_iff_isSimple

L508 ↗
FieldArithmetic.Chapter06.AffinePlaneCurve.isNormalAt_iff_isSimple
Documentation

Fried--Jarden, Lemma 6.2.3: a rational point of an irreducible affine plane curve is normal if and only if it is simple.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace AffinePlaneCurve
open IsLocalRing MvPolynomial
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem isNormalAt_iff_isSimple
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) :
    IsNormalAt p ↔ IsSimple p

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