Module

PartialDerivatives.lean

Nyll.SchemeTheory.PlaneCurves.PartialDerivatives

3 declarations indexed from sourceView source ↗

Module documentation

Partial derivatives on affine plane curves

This file develops the first-order polynomial decomposition used in Fried--Jarden, Lemma 6.2.3. Besides writing a polynomial minus its value at a point as a combination of the two translated coordinates, the construction controls the values of both coefficients: they are the two partial derivatives at the point.

Imports4

Nyll.SchemeTheory.PlaneCurves.CoordinateRing
Mathlib.Algebra.MvPolynomial.PDeriv
Mathlib.Tactic.FinCases
Mathlib.Tactic.LinearCombination

Imported by3

def

partialAt

L35 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.partialAt

Documentation

The value at p of the i-th formal partial derivative of f.

Source context 7 commands

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

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

Lean source · statement

def partialAt
    {f : BivariatePolynomial K} (p : RationalPoint f) (i : Fin 2) : K

def

IsSimple

L40 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.IsSimple

Documentation

A rational point is simple when some partial derivative is nonzero.

Source context 7 commands

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

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

Lean source · statement

def IsSimple
    {f : BivariatePolynomial K} (p : RationalPoint f) : Prop

theorem

exists_coordinate_decomposition_with_partialAt

L48 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.exists_coordinate_decomposition_with_partialAt

Documentation

First-order decomposition at a rational point, with exact control of the values of the two coefficients.

Source context 7 commands

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

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

Lean source · statement

theorem exists_coordinate_decomposition_with_partialAt
    {f : BivariatePolynomial K} (p : RationalPoint f)
    (g : BivariatePolynomial K) :
    ∃ u v : BivariatePolynomial K,
      g - MvPolynomial.C (polynomialEval p g) =
          (MvPolynomial.X 0 - MvPolynomial.C (p.coords 0)) * u +
            (MvPolynomial.X 1 - MvPolynomial.C (p.coords 1)) * v ∧
        polynomialEval p u =
          polynomialEval p (MvPolynomial.pderiv 0 g) ∧
        polynomialEval p v =
          polynomialEval p (MvPolynomial.pderiv 1 g)

Module documentation

Partial derivatives on affine plane curves

Declarations

partialAt

IsSimple

exists_coordinate_decomposition_with_partialAt