Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.PlaneCurveRatFuncModel

A rational-function-field model for a plane curve #

The first coordinate of an irreducible plane curve with nonzero second partial derivative is separating and transcendental. This file uses that coordinate to put the function field over the standard field K(X). It then transports finiteness, separability, and the exact extension degree from the intrinsic first-coordinate subfield.

This is the model required by the exhaustive finite-plus-infinity divisor formalization: its base is literally RatFunc K, and X specializes to the first coordinate function.

source
@[reducible]
noncomputable def BGS.CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hx : Transcendental K (planeCurveFunction f 0)) :
Algebra (RatFunc K) (PlaneCurveFunctionField f)

The RatFunc K-algebra structure obtained by specializing X at the first coordinate of the plane curve.

Equations
Instances For
    source
    @[simp]
    theorem BGS.CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra_algebraMap_apply {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hx : Transcendental K (planeCurveFunction f 0)) (z : RatFunc K) :
    (algebraMap (RatFunc K) (PlaneCurveFunctionField f)) z = (ratFuncSpecialization (planeCurveFunction f 0) hx) z
    source
    theorem BGS.CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra_X {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hx : Transcendental K (planeCurveFunction f 0)) :
    (algebraMap (RatFunc K) (PlaneCurveFunctionField f)) RatFunc.X = planeCurveFunction f 0
    source
    theorem BGS.CorvajaZannier.finiteDimensional_planeCurveFunctionField_over_ratFunc {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) :
    have hx := ⋯; FiniteDimensional (RatFunc K) (PlaneCurveFunctionField f)

    The plane-curve function field is finite over the standard rational function field when X is specialized to the first coordinate.

    source
    theorem BGS.CorvajaZannier.separable_planeCurveFunctionField_over_ratFunc {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) :
    have hx := ⋯; Algebra.IsSeparable (RatFunc K) (PlaneCurveFunctionField f)

    The same change of base transports separability.

    source
    theorem BGS.CorvajaZannier.finrank_planeCurveFunctionField_over_ratFunc_eq_degreeOf_second {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) :
    have hx := ⋯; Module.finrank (RatFunc K) (PlaneCurveFunctionField f) = MvPolynomial.degreeOf 1 f

    The extension degree over K(X) is exactly the degree of the equation in the second coordinate.

    The symmetric second-coordinate model #

    source
    @[reducible]
    noncomputable def BGS.CorvajaZannier.planeCurveSecondCoordinateRatFuncAlgebra {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hy : Transcendental K (planeCurveFunction f 1)) :
    Algebra (RatFunc K) (PlaneCurveFunctionField f)

    The RatFunc K-algebra structure obtained by specializing X at the second coordinate of the plane curve.

    Equations
    Instances For
      source
      @[simp]
      theorem BGS.CorvajaZannier.planeCurveSecondCoordinateRatFuncAlgebra_X {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hy : Transcendental K (planeCurveFunction f 1)) :
      (algebraMap (RatFunc K) (PlaneCurveFunctionField f)) RatFunc.X = planeCurveFunction f 1
      source
      theorem BGS.CorvajaZannier.finiteDimensional_planeCurveFunctionField_over_secondRatFunc {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) :
      have hy := ⋯; FiniteDimensional (RatFunc K) (PlaneCurveFunctionField f)

      The second-coordinate specialization also makes the plane-curve function field finite over the standard rational-function field.

      source
      theorem BGS.CorvajaZannier.separable_planeCurveFunctionField_over_secondRatFunc {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) :
      have hy := ⋯; Algebra.IsSeparable (RatFunc K) (PlaneCurveFunctionField f)

      The second-coordinate change of base transports separability.

      source
      theorem BGS.CorvajaZannier.finrank_planeCurveFunctionField_over_secondRatFunc_eq_degreeOf_first {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) :
      have hy := ⋯; Module.finrank (RatFunc K) (PlaneCurveFunctionField f) = MvPolynomial.degreeOf 0 f

      In the second-coordinate model the extension degree is exactly the degree of the equation in the first coordinate.