Powered-image index from an exact support determinant

The general powered-image theorem replaces a support determinant by its bidegree-box bound. This module retains a supplied support triple and hence its exact determinant. It is useful for sparse curves whose support lattice has much smaller index than the ambient degree box.

theorem BGS.CorvajaZannier.finrank_poweredCoordinateImageField_le_supportDet_isAlgClosed {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) {r s t : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hs : s ∈ f.support) (ht : t ∈ f.support) (hdet : planeCurveSupportDifferenceDet r s t ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmF : ↑m ≠ 0) (hnF : ↑n ≠ 0) : Module.finrank (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f) ≤ (planeCurveSupportDifferenceDet r s t).natAbs

Over algebraically closed constants, the source-to-powered-image degree is bounded by any nonzero determinant exhibited by three support monomials.

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le_supportDet_isAlgClosed {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) {r s t : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hs : s ∈ f.support) (ht : t ∈ f.support) (hdet : planeCurveSupportDifferenceDet r s t ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmF : ↑m ≠ 0) (hnF : ↑n ≠ 0) : Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ (planeCurveSupportDifferenceDet r s t).natAbs

The determinant-sensitive algebraically closed bound in the first-coordinate presentation used by Proposition Two.

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le_supportDet_of_nonzero_natCast {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) {r s t : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hs : s ∈ f.support) (ht : t ∈ f.support) (hdet : planeCurveSupportDifferenceDet r s t ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmK : ↑m ≠ 0) (hnK : ↑n ≠ 0) : have hf := ⋯; Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ (planeCurveSupportDifferenceDet r s t).natAbs

Exact-support index bound over arbitrary constants, obtained by the same base-change descent as the public bidegree theorem.

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le_supportDet {p : ℕ} {K : Type u_1} [Field K] [CharP K p] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) {r s t : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hs : s ∈ f.support) (ht : t ∈ f.support) (hdet : planeCurveSupportDifferenceDet r s t ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmPrime : ¬p ∣ m) (hnPrime : ¬p ∣ n) : have hf := ⋯; Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ (planeCurveSupportDifferenceDet r s t).natAbs

Prime-to-characteristic powers satisfy the exact-support index bound.