The common source-to-powered-image index

The powered image field is presented twice, once over each powered coordinate. Although these presentations have different base fields, their underlying intermediate field in the source function field is the same. This file transports finrank across IntermediateField.restrictScalars, identifies the two source-to-image indices, and records the elementary projection bounds.

These statements do not identify image-curve degrees with source heights. The missing exponent-independent bound on the common index is a genuinely additional logarithmic-geometric input.

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_eq_imageField {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) = Module.finrank (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f)

The first-coordinate presentation has the same source degree as the common powered image field K(x^m,y^n).

theorem BGS.CorvajaZannier.finrank_poweredImageOverSecond_eq_imageField {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : Module.finrank (↥(PoweredImageOverSecond f m n)) (PlaneCurveFunctionField f) = Module.finrank (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f)

The second-coordinate presentation has the same source degree as the common powered image field K(x^m,y^n).

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_eq_poweredImageOverSecond {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) = Module.finrank (↥(PoweredImageOverSecond f m n)) (PlaneCurveFunctionField f)

Both relative presentations compute one and the same geometric degree of the source-to-powered-image map.

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le_firstProjectionPowerDegree {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 : ℕ) : Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ m * MvPolynomial.degreeOf 1 f

The common powered-image index is at most the source degree over the powered first coordinate, hence at most m * degreeOf 1 f.

theorem BGS.CorvajaZannier.finrank_poweredImageOverSecond_le_secondProjectionPowerDegree {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (m n : ℕ) (hn : 0 < n) : Module.finrank (↥(PoweredImageOverSecond f m n)) (PlaneCurveFunctionField f) ≤ n * MvPolynomial.degreeOf 0 f

The common powered-image index is at most the source degree over the powered second coordinate, hence at most n * degreeOf 0 f.