Prove2Me

Chain rule in C(t)[W]/(W2−h)\mathbb C(t)[W]/(W^2-h): d(p(t))=p′(t) dtd\big(p(t)\big)=p'(t)\,dt for every polynomial pp

Proved
CurveSymmetry.quad_D_algebraMap

by carlok · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

curve-symmetry-leanfunction-fieldskahler-differentials

Let h∈C[t]h\in\mathbb C[t] be such that W2−h(t)W^2-h(t) is irreducible in C(t)[W]\mathbb C(t)[W], let Lh=C(t)[W]/(W2−h(t))L_h=\mathbb C(t)[W]/(W^2-h(t)), and let d ⁣:Lh→ΩLh/Cd\colon L_h\to\Omega_{L_h/\mathbb C} be the universal derivation into the Kähler differentials of LhL_h over C\mathbb C. Then for every polynomial p∈C[t]p\in\mathbb C[t], viewed as an element of LhL_h,

d(p(t))=p′(t) dt,d\big(p(t)\big)=p'(t)\,dt,

where p′p' is the derivative of pp.

This chain rule along C[t]→Lh\mathbb C[t]\to L_h is used to differentiate the relation w2=h(t)w^2=h(t) and other polynomial expressions in tt when the differentials of the double cover (7) are computed, for the genus in Lemma 4 and for Remark 5.

Formalization Note: the irreducibility of W2−h(t)W^2-h(t) is a Fact instance.

Preamble
import Definitions.Def_CurveSymmetry_01_RealLoci
import Definitions.Def_CurveSymmetry_02_FamilyBasics
import Definitions.Def_CurveSymmetry_03_IsometriesAndCharts
import Definitions.Def_CurveSymmetry_05_FamilyFunctionField
import Definitions.Def_CurveSymmetry_06_QuadraticRing
import Definitions.Def_CurveSymmetry_08_Differentials
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.MvPolynomial.PDeriv
import Mathlib.Algebra.Polynomial.FieldDivision
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Algebra.Polynomial.SpecificDegree
import Mathlib.Analysis.Complex.Isometry
import Mathlib.Analysis.Complex.OperatorNorm
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Analysis.Normed.Affine.MazurUlam
import Mathlib.Data.Complex.Basic
import Mathlib.FieldTheory.RatFunc.Basic
import Mathlib.FieldTheory.Separable
import Mathlib.LinearAlgebra.Basis.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import Mathlib.LinearAlgebra.TensorProduct.Basis
import Mathlib.RingTheory.AdjoinRoot
import Mathlib.RingTheory.Etale.Field
import Mathlib.RingTheory.Etale.Kaehler
import Mathlib.RingTheory.Kaehler.Polynomial
import Mathlib.RingTheory.MvPolynomial.Homogeneous
import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
import Mathlib.RingTheory.Polynomial.GaussLemma
import Mathlib.RingTheory.RootsOfUnity.Complex
import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
import Mathlib.Tactic

open CurveSymmetry
set_option autoImplicit false
open Polynomial TensorProduct
variable (h : ℂ[X]) [Fact (Irreducible (quadRat h))]
Formal statement
theorem CurveSymmetry.quad_D_algebraMap (p : ℂ[X]) :
    KaehlerDifferential.D ℂ (QuadField h) (algebraMap ℂ[X] (QuadField h) p) =
      algebraMap ℂ[X] (QuadField h) p.derivative •
        KaehlerDifferential.D ℂ (QuadField h) (quadT h) := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for Lemma 4, pp. 3-4, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/QuadraticDifferentials.lean (C. Perassi)

View graph