NYLL
Module

MonicChange.lean

Nyll.SchemeTheory.PlaneCurves.MonicChange
22 declarations indexed from sourceView source ↗

Module documentation

Monic linear representatives of plane curves

This file connects the linear normalization developed for Fried--Jarden, Proposition 6.2.1, with the monic projection model. Over an infinite field, an invertible linear change of the two affine coordinates makes the leading coefficient in the projection variable a unit. Multiplication by that unit's inverse then gives a monic equation defining the same principal ideal.

Imports3
Imported by3

Declarations

def

linearChangeY

L39 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.linearChangeY
Documentation

Conjugate the triangular change from LinearNormalization by the exchange of the two plane coordinates. In the asPolynomialY presentation this is exactly linearChangeFirst.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def linearChangeY (c : Fin 1 → K) :
    BivariatePolynomial K ≃ₐ[K] BivariatePolynomial K
theorem

rename_linearChangeY

L45 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.rename_linearChangeY
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem rename_linearChangeY
    (c : Fin 1 → K) (f : BivariatePolynomial K) :
    MvPolynomial.rename coordinateSwap (linearChangeY c f) =
      linearChangeFirst c (MvPolynomial.rename coordinateSwap f)
theorem

yPolynomial_linearChangeY

L51 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.yPolynomial_linearChangeY
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem yPolynomial_linearChangeY
    (c : Fin 1 → K) (f : BivariatePolynomial K) :
    yPolynomial (linearChangeY c f) =
      MvPolynomial.finSuccEquiv K 1
        (linearChangeFirst c (MvPolynomial.rename coordinateSwap f))
theorem

exists_linearChangeY_leadingCoeff_isUnit

L62 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.exists_linearChangeY_leadingCoeff_isUnit
Documentation

Over an infinite field, an invertible linear change makes the leading coefficient of the Y-polynomial a unit of K[X].

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem exists_linearChangeY_leadingCoeff_isUnit
    [Infinite K] {f : BivariatePolynomial K} (hf : f ≠ 0) :
    ∃ c : Fin 1 → K,
      IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff
theorem

totalDegree_linearChangeFirst_le

L74 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.totalDegree_linearChangeFirst_le
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem totalDegree_linearChangeFirst_le
    {n : ℕ} (c : Fin n → K)
    (f : MvPolynomial (Fin (n + 1)) K) :
    (linearChangeFirst c f).totalDegree ≤ f.totalDegree
theorem

totalDegree_linearChangeFirst

L100 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.totalDegree_linearChangeFirst
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem totalDegree_linearChangeFirst
    {n : ℕ} (c : Fin n → K)
    (f : MvPolynomial (Fin (n + 1)) K) :
    (linearChangeFirst c f).totalDegree = f.totalDegree
theorem

totalDegree_linearChangeY

L119 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.totalDegree_linearChangeY
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem totalDegree_linearChangeY
    (c : Fin 1 → K) (f : BivariatePolynomial K) :
    (linearChangeY c f).totalDegree = f.totalDegree
def

normalizeLeadingUnit

L139 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.normalizeLeadingUnit
Documentation

Multiply a polynomial by the inverse of its unit leading coefficient.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def normalizeLeadingUnit
    (p : Polynomial (ProjectionBase K)) (h : IsUnit p.leadingCoeff) :
    Polynomial (ProjectionBase K)
theorem

normalizeLeadingUnit_monic

L144 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.normalizeLeadingUnit_monic
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem normalizeLeadingUnit_monic
    (p : Polynomial (ProjectionBase K)) (h : IsUnit p.leadingCoeff) :
    (normalizeLeadingUnit p h).Monic
theorem

normalizeLeadingUnit_associated

L153 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.normalizeLeadingUnit_associated
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem normalizeLeadingUnit_associated
    (p : Polynomial (ProjectionBase K)) (h : IsUnit p.leadingCoeff) :
    Associated (normalizeLeadingUnit p h) p
def

monicRepresentative

L163 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.monicRepresentative
Documentation

The monic plane equation obtained from a chosen linear change whose leading coefficient is a unit.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def monicRepresentative
    (f : BivariatePolynomial K) (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    BivariatePolynomial K
theorem

yPolynomial_monicRepresentative

L171 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.yPolynomial_monicRepresentative
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem yPolynomial_monicRepresentative
    (f : BivariatePolynomial K) (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    yPolynomial (monicRepresentative f c h) =
      normalizeLeadingUnit (yPolynomial (linearChangeY c f)) h
theorem

monicRepresentative_monic

L178 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.monicRepresentative_monic
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem monicRepresentative_monic
    (f : BivariatePolynomial K) (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    (yPolynomial (monicRepresentative f c h)).Monic
theorem

monicRepresentative_associated

L185 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.monicRepresentative_associated
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem monicRepresentative_associated
    (f : BivariatePolynomial K) (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    Associated (monicRepresentative f c h) (linearChangeY c f)
theorem

equationIdeal_monicRepresentative

L201 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.equationIdeal_monicRepresentative
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem equationIdeal_monicRepresentative
    (f : BivariatePolynomial K) (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    equationIdeal (monicRepresentative f c h) =
      equationIdeal (linearChangeY c f)
theorem

map_equationIdeal_linearChangeY

L210 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.map_equationIdeal_linearChangeY
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem map_equationIdeal_linearChangeY
    (f : BivariatePolynomial K) (c : Fin 1 → K) :
    (equationIdeal f).map (linearChangeY c).toRingEquiv.toRingHom =
      equationIdeal (linearChangeY c f)
def

coordinateRingEquivLinearChangeY

L219 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.coordinateRingEquivLinearChangeY
Documentation

The invertible linear change descends to the two coordinate rings.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def coordinateRingEquivLinearChangeY
    (f : BivariatePolynomial K) (c : Fin 1 → K) :
    CoordinateRing f ≃ₐ[K] CoordinateRing (linearChangeY c f)
def

coordinateRingEquivMonicRepresentative

L232 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.coordinateRingEquivMonicRepresentative
Documentation

The original plane equation and its monic representative have isomorphic coordinate rings.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def coordinateRingEquivMonicRepresentative
    (f : BivariatePolynomial K) (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    CoordinateRing f ≃ₐ[K] CoordinateRing (monicRepresentative f c h)
theorem

totalDegree_monicRepresentative

L240 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.totalDegree_monicRepresentative
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem totalDegree_monicRepresentative
    {f : BivariatePolynomial K} (hf : f ≠ 0)
    (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    (monicRepresentative f c h).totalDegree = f.totalDegree
theorem

monicRepresentative_irreducible

L262 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.monicRepresentative_irreducible
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem monicRepresentative_irreducible
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    Irreducible (monicRepresentative f c h)
def

functionFieldEquivMonicRepresentative

L274 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.functionFieldEquivMonicRepresentative
Documentation

The induced equivalence of plane-curve function fields.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def functionFieldEquivMonicRepresentative
    {f : BivariatePolynomial K} (_hf : Irreducible f)
    (c : Fin 1 → K)
    (h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff) :
    FractionRing (CoordinateRing f) ≃ₐ[K]
      FractionRing (CoordinateRing (monicRepresentative f c h))
theorem

exists_irreducible_monicRepresentative

L293 ↗
FieldArithmetic.Chapter06.PlaneCurveMonicNormalization.exists_irreducible_monicRepresentative
Documentation

Existence of an irreducible monic representative after an invertible linear change, over an infinite field.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PlaneCurveMonicNormalization
open MvPolynomial Polynomial
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem exists_irreducible_monicRepresentative
    [Infinite K] {f : BivariatePolynomial K} (hf : Irreducible f) :
    ∃ c : Fin 1 → K,
      ∃ h : IsUnit (yPolynomial (linearChangeY c f)).leadingCoeff,
        Irreducible (monicRepresentative f c h) ∧
          (yPolynomial (monicRepresentative f c h)).Monic ∧
            (monicRepresentative f c h).totalDegree =
              f.totalDegree

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