Coefficientwise integer lifts preserve homogeneous weights and origin-ideal powers.

noncomputable def CCDN.modularPolynomialLift {σ : Type u_1} {p : ℕ} (f : MvPolynomial σ (ZMod p)) : MvPolynomial σ ℤ

The integer polynomial lifting a polynomial over ZMod p coefficientwise, using the representatives ZMod.val in [0, p).

Equations

• CCDN.modularPolynomialLift f = ∑ e ∈ f.support, (MvPolynomial.monomial e) ↑(f.coeff e).val

theorem CCDN.map_modularPolynomialLift {σ : Type u_1} {p : ℕ} [NeZero p] (f : MvPolynomial σ (ZMod p)) : (MvPolynomial.map (Int.castRingHom (ZMod p))) (modularPolynomialLift f) = f

Reducing the coefficientwise lift of f modulo p recovers f.

theorem CCDN.modularPolynomialLift_homogeneous {σ : Type u_1} {p k : ℕ} (f : MvPolynomial σ (ZMod p)) (hf : f.IsHomogeneous k) : (modularPolynomialLift f).IsHomogeneous k

The coefficientwise lift of a homogeneous polynomial of degree k over ZMod p is homogeneous of degree k.

theorem CCDN.modularPolynomialLift_mem_origin_power {σ : Type u_1} {p k : ℕ} (f : MvPolynomial σ (ZMod p)) (hf : f ∈ MvPolynomial.idealOfVars σ (ZMod p) ^ k) : modularPolynomialLift f ∈ MvPolynomial.idealOfVars σ ℤ ^ k

If f lies in the k-th power of the ideal of the origin over ZMod p, then so does its coefficientwise lift over ℤ.