Uniform finite p-adic approximation by weighted local generators at a possibly singular plane-curve residue point.
theorem
CCDN.origin_power_eval_dvd
{σ : Type u_1}
(p : ℤ)
(x : σ → ℤ)
(hx : ∀ (j : σ), p ∣ x j)
{N : ℕ}
{u : MvPolynomial σ ℤ}
(hu : u ∈ MvPolynomial.idealOfVars σ ℤ ^ N)
:
If every coordinate of x is divisible by p, then p ^ N divides u(x) for every integer
polynomial u in the N-th power of the ideal of the origin.
theorem
CCDN.integer_generators_approximate_mod
{σ : Type u_1}
{p N : ℕ}
(f : MvPolynomial σ ℤ)
(r : ℕ → ℕ)
(g : (k : ℕ) → Fin (r k) → MvPolynomial σ ℤ)
(hrep :
∀ (u : MvPolynomial σ ℤ),
∃ (c : (k : Fin N) → Fin (r ↑k) → ℤ) (h : MvPolynomial σ ℤ) (v : MvPolynomial σ ℤ) (w : MvPolynomial σ ℤ),
v ∈ MvPolynomial.idealOfVars σ ℤ ^ N ∧ u - ∑ k : Fin N, ∑ j : Fin (r ↑k), c k j • g (↑k) j = f * h + v + MvPolynomial.C ↑p * w)
(u : MvPolynomial σ ℤ)
:
Iterating the explicit p-divisible error yields a representation to any fixed precision, uniformly over every integral zero in the origin residue class.
theorem
CCDN.exists_singular_plane_approximation_mod
{p μ : ℕ}
[Fact (Nat.Prime p)]
(f : MvPolynomial (Fin 2) ℤ)
(hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ μ)
(hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) ≠ 0)
:
∃ (r : ℕ → ℕ) (g : (k : ℕ) → Fin (r k) → MvPolynomial (Fin 2) ℤ),
(∀ (k : ℕ), r k ≤ μ) ∧ (∀ (k : ℕ) (j : Fin (r k)), (g k j).IsHomogeneous k) ∧ ∀ (N : ℕ) (u : MvPolynomial (Fin 2) ℤ),
∃ (c : (k : Fin N) → Fin (r ↑k) → ℤ),
∀ (x : Fin 2 → ℤ),
↑p ^ N ∣ (MvPolynomial.eval x) f →
(∀ (j : Fin 2), ↑p ∣ x j) →
↑p ^ N ∣ (MvPolynomial.eval x) u - ∑ k : Fin N, ∑ j : Fin (r ↑k), c k j * (MvPolynomial.eval x) (g (↑k) j)
For a plane equation of multiplicity μ at the origin modulo p, a family of at most μ
integer homogeneous generators in each degree approximates every polynomial modulo p^N at all
zeros of f modulo p^N divisible by p, with one choice of coefficients for all such zeros.
This permits normalization of projective points modulo prime powers.