Exact degree of a transcendental power map

For a transcendental element z, the extension K(z)/K(z^m) has exact degree m. The key polynomial is Eisenstein at the rational parameter.

theorem BGS.CorvajaZannier.minpoly_natDegree_over_adjoin_pow_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (hz : Transcendental K z) (m : ℕ) (hm : 0 < m) : (minpoly (↥K⟮z ^ m⟯) z).natDegree = m

A transcendental element has minimal polynomial of degree m over the field generated by its m-th power.

theorem BGS.CorvajaZannier.finrank_adjoin_over_adjoin_pow_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (hz : Transcendental K z) (m : ℕ) (hm : 0 < m) : Module.finrank ↥K⟮z ^ m⟯ ↥(↥K⟮z ^ m⟯)⟮z⟯ = m

The simple extension generated by a transcendental element over the field generated by its power has exact degree m.

theorem BGS.CorvajaZannier.finrank_over_adjoin_pow_eq_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (hz : Transcendental K z) (m : ℕ) (hm : 0 < m) [FiniteDimensional (↥K⟮z⟯) L] : Module.finrank (↥K⟮z ^ m⟯) L = m * Module.finrank (↥K⟮z⟯) L

Passing from K(z) to K(z^m) multiplies the degree of any finite top extension by exactly m.

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

Exact source degree over the powered first coordinate.

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

Exact source degree over the powered second coordinate.