Exact source-height factorization through the powered image

These identities are the degree bookkeeping used in the two orientations of Corvaja--Zannier Proposition 2. The first factor is the relevant degree of the powered-image relation and the second is the common source-to-image index.

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_transpose_natDegree_mul_commonIndex {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 n : ℕ) (hm : 0 < m) (hn : 0 < n) : (transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree * Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) = n * MvPolynomial.degreeOf 0 f

In the orientation (u,v)=(x^m,y^n), the degree of the image relation in u times the common source-to-image index is the source height n d₀.

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

In the swapped orientation (u,v)=(y^n,x^m), the degree of the image relation in y^n times the same index is the source height m d₁.