NYLL
Module

MonicProjection.lean

Nyll.SchemeTheory.PlaneCurves.MonicProjection
29 declarations indexed from sourceView source ↗

Module documentation

Monic projections of affine plane curves

This file isolates the finite-degree input used in Fried--Jarden, Lemma 6.2.2(b),(d). If the equation of a plane curve is monic in Y, its coordinate ring is a finite free algebra over the polynomial ring in X. After passing to fraction fields, the same rank is the degree in Y, hence is bounded by the total degree of the equation.

Imports5
Imported by4

Declarations

abbrev

ProjectionBase

L38 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.ProjectionBase
Documentation

The coefficient ring K[X], represented as the one-variable multivariate polynomial ring used by MvPolynomial.finSuccEquiv.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
abbrev ProjectionBase (K : Type u) [Field K]
abbrev

ProjectionFunctionField

L42 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.ProjectionFunctionField
Documentation

The rational function field K(X).

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
abbrev ProjectionFunctionField (K : Type u) [Field K]
def

coordinateSwap

L46 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateSwap
Documentation

Exchange the two affine coordinates.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
def coordinateSwap : Fin 2 ≃ Fin 2
def

asPolynomialY

L53 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.asPolynomialY
Documentation

View a bivariate polynomial as a polynomial in the original Y variable with coefficients in K[X].

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
def asPolynomialY :
    BivariatePolynomial K ≃ₐ[K] Polynomial (ProjectionBase K)
def

yPolynomial

L59 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.yPolynomial
Documentation

A bivariate equation, viewed as a polynomial in Y over K[X].

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
def yPolynomial (f : BivariatePolynomial K) :
    Polynomial (ProjectionBase K)
def

degreeY

L64 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.degreeY
Documentation

The degree of a bivariate equation in Y.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
def degreeY (f : BivariatePolynomial K) : ℕ
theorem

asPolynomialY_apply

L68 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.asPolynomialY_apply
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem asPolynomialY_apply (f : BivariatePolynomial K) :
    asPolynomialY f =
      MvPolynomial.finSuccEquiv K 1
        (MvPolynomial.rename coordinateSwap f)
theorem

asPolynomialY_X

L75 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.asPolynomialY_X
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem asPolynomialY_X :
    asPolynomialY (K := K) (MvPolynomial.X (R := K) (0 : Fin 2)) =
      Polynomial.C (MvPolynomial.X (R := K) (0 : Fin 1))
theorem

asPolynomialY_Y

L88 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.asPolynomialY_Y
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem asPolynomialY_Y :
    asPolynomialY (K := K) (MvPolynomial.X (R := K) (1 : Fin 2)) =
      (Polynomial.X : Polynomial (ProjectionBase K))
theorem

degreeY_le_totalDegree

L99 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.degreeY_le_totalDegree
Documentation

Degree in Y is bounded by total degree.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem degreeY_le_totalDegree (f : BivariatePolynomial K) :
    degreeY f ≤ MvPolynomial.totalDegree f
theorem

yPolynomial_irreducible

L110 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.yPolynomial_irreducible
Documentation

Irreducibility is preserved by viewing the equation as a polynomial in Y.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem yPolynomial_irreducible
    {f : BivariatePolynomial K} (hf : Irreducible f) :
    Irreducible (yPolynomial f)
theorem

degreeY_pos

L116 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.degreeY_pos
Documentation

An irreducible monic equation has positive degree in Y.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem degreeY_pos
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    0 < degreeY f
abbrev

ProjectionModel

L128 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.ProjectionModel
Documentation

The polynomial-quotient model attached to the Y-projection.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
abbrev ProjectionModel (f : BivariatePolynomial K)
theorem

mapped_equationIdeal

L131 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.mapped_equationIdeal
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem mapped_equationIdeal (f : BivariatePolynomial K) :
    (equationIdeal f).map
      (asPolynomialY (K := K)).toRingEquiv.toRingHom =
      Ideal.span ({yPolynomial f} : Set _)
def

coordinateRingEquivProjectionModel

L140 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRingEquivProjectionModel
Documentation

The coordinate ring and the polynomial quotient are canonically equivalent as K-algebras.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
def coordinateRingEquivProjectionModel (f : BivariatePolynomial K) :
    CoordinateRing f ≃ₐ[K] ProjectionModel f
def

projectionAlgebra

L153 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.projectionAlgebra
Documentation

The K[X]-algebra structure on the coordinate ring induced by projection to the X-axis.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
def projectionAlgebra (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f)
instance

projectionAlgebraInstance

L158 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.projectionAlgebraInstance
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
Lean source · statement
instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f)
def

coordinateRingEquivProjection

L163 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRingEquivProjection
Documentation

The polynomial-quotient equivalence, now over the projection base.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
def coordinateRingEquivProjection (f : BivariatePolynomial K) :
    @AlgEquiv (ProjectionBase K) (CoordinateRing f) (ProjectionModel f)
      _ _ _ (projectionAlgebra f) _
def

coordinateRingPowerBasis

L174 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRingPowerBasis
Documentation

The monic quotient power basis, transported to the coordinate ring.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
def coordinateRingPowerBasis
    (f : BivariatePolynomial K) (hf : (yPolynomial f).Monic) :
    @PowerBasis (ProjectionBase K) (CoordinateRing f)
      _ _ (projectionAlgebra f)
theorem

coordinateRingPowerBasis_dim

L186 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRingPowerBasis_dim
Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem coordinateRingPowerBasis_dim
    (f : BivariatePolynomial K) (hf : (yPolynomial f).Monic) :
    (coordinateRingPowerBasis f hf).dim = degreeY f
theorem

coordinateRing_moduleFinite

L192 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRing_moduleFinite
Documentation

A monic plane-curve coordinate ring is finite free over K[X].

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem coordinateRing_moduleFinite
    (f : BivariatePolynomial K) (hf : (yPolynomial f).Monic) :
    @Module.Finite (ProjectionBase K) (CoordinateRing f)
      _ _ (projectionAlgebra f).toModule
theorem

coordinateRing_moduleFree

L201 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRing_moduleFree
Documentation

A monic plane-curve coordinate ring is free over K[X].

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem coordinateRing_moduleFree
    (f : BivariatePolynomial K) (hf : (yPolynomial f).Monic) :
    @Module.Free (ProjectionBase K) (CoordinateRing f)
      _ _ (projectionAlgebra f).toModule
theorem

coordinateRing_finrank

L211 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRing_finrank
Documentation

The module rank of a monic plane-curve coordinate ring is its degree in Y.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem coordinateRing_finrank
    (f : BivariatePolynomial K) (hf : (yPolynomial f).Monic) :
    @Module.finrank (ProjectionBase K) (CoordinateRing f)
      _ _ (projectionAlgebra f).toModule =
      degreeY f
theorem

coordinateRing_isIntegral

L222 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.coordinateRing_isIntegral
Documentation

Module-finiteness supplies integrality of the coordinate ring over K[X].

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem coordinateRing_isIntegral
    (f : BivariatePolynomial K) (hf : (yPolynomial f).Monic) :
    @Algebra.IsIntegral (ProjectionBase K) (CoordinateRing f)
      _ _ (projectionAlgebra f)
theorem

projectionAlgebra_injective

L234 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.projectionAlgebra_injective
Documentation

The projection map K[X] → K[X,Y]/(f) is injective when the transformed equation is irreducible and monic.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem projectionAlgebra_injective
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    Function.Injective
      (@algebraMap (ProjectionBase K) (CoordinateRing f)
        _ _ (projectionAlgebra f))
def

functionFieldAlgebra

L259 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.functionFieldAlgebra
Documentation

The field extension K(X) → Frac(K[X,Y]/(f)) induced by the monic projection. Irreducibility supplies the domain structure, while monicity supplies injectivity of the map from K[X].

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
def functionFieldAlgebra
    (f : BivariatePolynomial K) (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    Algebra (ProjectionFunctionField K) (FractionRing (CoordinateRing f))
theorem

functionField_finiteDimensional

L274 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.functionField_finiteDimensional
Documentation

The function field is finite-dimensional over K(X).

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem functionField_finiteDimensional
    (f : BivariatePolynomial K) (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    @Module.Finite (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) _ _
      (functionFieldAlgebra f hirr hmonic).toModule
theorem

functionField_finrank

L303 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.functionField_finrank
Documentation

Passing to fraction fields preserves the power-basis rank.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem functionField_finrank
    (f : BivariatePolynomial K) (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    @Module.finrank (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) _ _
      (functionFieldAlgebra f hirr hmonic).toModule =
      degreeY f
theorem

functionField_finrank_le_totalDegree

L332 ↗
FieldArithmetic.Chapter06.MonicPlaneCurveProjection.functionField_finrank_le_totalDegree
Documentation

The function-field degree is bounded by the total degree of the plane equation.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace MonicPlaneCurveProjection
open MvPolynomial Polynomial
open AffinePlaneCurve
universe u
variable {K : Type u} [Field K]
local instance projectionAlgebraInstance (f : BivariatePolynomial K) :
    Algebra (ProjectionBase K) (CoordinateRing f) :=
  projectionAlgebra f
Lean source · statement
theorem functionField_finrank_le_totalDegree
    (f : BivariatePolynomial K) (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    @Module.finrank (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) _ _
      (functionFieldAlgebra f hirr hmonic).toModule ≤
      MvPolynomial.totalDegree f

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