From the public bidegree interface to function-field degrees

The finite-field Corvaja--Zannier endpoint states its degree hypothesis support-wise, through BGS.External.HasBidegreeAtMost. The function-field development uses MvPolynomial.degreeOf and the degrees of the two coordinate projections. This file records the exact, assumption-free bridge between those two presentations.

theorem BGS.CorvajaZannier.degreeOf_first_le_of_hasBidegreeAtMost {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : MvPolynomial.degreeOf 0 f ≤ firstDegree

The first coordinate degree is bounded by the first component of a support-wise bidegree bound.

theorem BGS.CorvajaZannier.degreeOf_second_le_of_hasBidegreeAtMost {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : MvPolynomial.degreeOf 1 f ≤ secondDegree

The second coordinate degree is bounded by the second component of a support-wise bidegree bound.

theorem BGS.CorvajaZannier.irreducible_of_irreducible_map_algebraicClosure {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : Irreducible f

Absolute irreducibility in the public plane-curve interface implies irreducibility over the original constant field.

theorem BGS.CorvajaZannier.finrank_over_firstCoordinate_le_of_hasBidegreeAtMost {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : Module.finrank (↥(FirstCoordinateSubfield f)) (PlaneCurveFunctionField f) ≤ secondDegree

The degree of the first-coordinate projection of the plane-curve function field is bounded by the supplied second bidegree.

theorem BGS.CorvajaZannier.finrank_over_secondCoordinate_le_of_hasBidegreeAtMost {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : Module.finrank (↥(SecondCoordinateSubfield f)) (PlaneCurveFunctionField f) ≤ firstDegree

The degree of the second-coordinate projection of the plane-curve function field is bounded by the supplied first bidegree.