Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.PoweredImageBaseChange

Constant-field base change for the powered-image index #

The canonical powered-image relation remains associated to its coefficient base change. Comparing the exact tower-degree factorizations on the two curves then shows that the source-to-powered-image finrank is invariant under extension of constants. This is the descent bridge from the algebraically closed stabilizer argument to the original constant field.

source
theorem BGS.CorvajaZannier.bivariateEvalAlgHom_map_mapRingHom {K : Type u_1} {E : Type u_2} {L : Type u_3} [Field K] [Field E] [CommRing L] [Algebra K E] [Algebra K L] [Algebra E L] [IsScalarTower K E L] (u v : L) (P : Polynomial (Polynomial K)) :
(bivariateEvalAlgHom u v) (Polynomial.map (Polynomial.mapRingHom (algebraMap K E)) P) = (bivariateEvalAlgHom u v) P

Bivariate evaluation commutes with an extension of the coefficient field.

source
noncomputable def BGS.CorvajaZannier.planeCurveCoordinateRingMap {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) :
PlaneCurveCoordinateRing f →ₐ[K] PlaneCurveCoordinateRing ((MvPolynomial.map (algebraMap K E)) f)

The coefficient-extension map between affine plane-curve coordinate rings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem BGS.CorvajaZannier.planeCurveCoordinateRingMap_coordinate {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (i : Fin 2) :
    (planeCurveCoordinateRingMap f) (planeCurveCoordinate f i) = planeCurveCoordinate ((MvPolynomial.map (algebraMap K E)) f) i

    The coordinate-ring base-change map preserves the two coordinate classes.

    source
    theorem BGS.CorvajaZannier.evalBivariate_poweredCoordinateImageRelation_map_eq_zero {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) :
    let fE := (MvPolynomial.map (algebraMap K E)) f; have g := poweredCoordinateImageRelation hf hpartialSecond m hm n; evalBivariate (planeCurveFunction fE 0 ^ m) (planeCurveFunction fE 1 ^ n) (Polynomial.map (Polynomial.mapRingHom (algebraMap K E)) g) = 0

    The coefficient base change of the canonical powered-image relation vanishes on the generic powered coordinates of the base-changed curve.

    source
    theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_map_associated_baseChange {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hpartialSecondE : (MvPolynomial.pderiv 1) ((MvPolynomial.map (algebraMap K E)) f) ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) :
    Associated (poweredCoordinateImageRelation hfE hpartialSecondE m hm n) (Polynomial.map (Polynomial.mapRingHom (algebraMap K E)) (poweredCoordinateImageRelation hf hpartialSecond m hm n))

    The canonical powered-image relation of the base-changed curve is associated to the coefficient base change of the original relation.

    source
    theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_map_natDegree_eq_baseChange {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hf : Irreducible f) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hpartialSecondE : (MvPolynomial.pderiv 1) ((MvPolynomial.map (algebraMap K E)) f) ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) :
    (poweredCoordinateImageRelation hfE hpartialSecondE m hm n).natDegree = (poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree

    The relevant powered-image relation degree is invariant under extension of constants.

    source
    theorem BGS.CorvajaZannier.finrank_poweredCoordinateImageField_eq_baseChange {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) :
    let fE := (MvPolynomial.map (algebraMap K E)) f; have hfE := ⋯; Module.finrank (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f) = Module.finrank (↥(PoweredCoordinateImageField fE m n)) (PlaneCurveFunctionField fE)

    Extension of constants preserves the common source-to-powered-image degree.