Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.PoweredImageHeightFactor

The source-to-powered-image degree factor #

The bidegrees of poweredCoordinateImageRelation are degrees on the powered image curve, whereas the divisor argument computes coordinate heights on the source curve. The discrepancy is exactly the degree of the finite map from the source curve to its powered image. These tower identities expose that factor explicitly.

source
theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_natDegree_mul_imageIndex {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) :
(poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree * Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) = Module.finrank (↥(FirstPoweredCoordinateSubfield f m)) (PlaneCurveFunctionField f)

The source degree over the powered first coordinate is the powered-image relation's degree in the second coordinate times the source-to-image degree.

source
theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_transpose_natDegree_mul_imageIndex {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) (hn : 0 < n) :
(transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree * Module.finrank (↥(PoweredImageOverSecond f m n)) (PlaneCurveFunctionField f) = Module.finrank (↥(SecondPoweredCoordinateSubfield f n)) (PlaneCurveFunctionField f)

The source degree over the powered second coordinate is the powered-image relation's degree in the first coordinate times the same geometric source-to-image degree, written in the second-coordinate presentation.