Finite bad-prime sets for plane equations, with coefficient-height charge bounds and irreducible good reductions.
theorem
CCDN.mvPolynomial_irreducible_of_field_map
{F : Type u_1}
{K : Type u_2}
{σ : Type u_3}
[Field F]
[Field K]
(φ : F →+* K)
(f : MvPolynomial σ F)
(hf : Irreducible ((MvPolynomial.map φ) f))
:
A multivariate polynomial over a field whose image under a field homomorphism is irreducible is itself irreducible.
The total degree of the bivariate model bivariatePolynomialEquiv R f of a polynomial f in
two variables equals the total degree of f.
theorem
CCDN.irreducible_reduction_of_not_hypersurfaceBadReduction
{σ : Type u_1}
(f : MvPolynomial σ ℤ)
(p : ℕ)
[Fact (Nat.Prime p)]
(hf : ¬HypersurfaceBadReduction f p)
:
Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)
Good reduction implies the irreducibility over the prime field needed by the singular determinant estimate.
theorem
CCDN.exists_plane_bad_prime_set
{F : Type u_1}
[Field F]
[CharZero F]
[IsAlgClosed F]
(f : MvPolynomial (Fin 2) ℤ)
(hd : 0 < f.totalDegree)
(hir : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f))
(H : ℝ)
(hH : 1 ≤ H)
(hcoeff : CoefficientHeightLE f H)
:
The complete set of bad primes above stepanovThreshold d is finite and has the
required charge bound. Good reductions outside this set are
irreducible reductions, not an additional input.