Bad reduction of an integer polynomial at a prime: degree loss or failure of absolute irreducibility modulo p.

def CCDN.HypersurfaceBadReduction {σ : Type u_1} (f : MvPolynomial σ ℤ) (p : ℕ) : Prop

Bad reduction at p: p is prime and the reduction of f over the algebraic closure of 𝔽_p either has smaller total degree than f or is not irreducible.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.not_hypersurfaceBadReduction_iff {σ : Type u_1} (f : MvPolynomial σ ℤ) (p : ℕ) [Fact (Nat.Prime p)] : ¬HypersurfaceBadReduction f p ↔ ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure (ZMod p)))) f).totalDegree = f.totalDegree ∧ Irreducible ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure (ZMod p)))) f)

At a prime p, good reduction means that the reduction over the algebraic closure of 𝔽_p keeps the total degree and is irreducible.