Positive singular multiplicity is derived from a nonzero equation vanishing at the origin; it is bounded by the equation's total degree.
theorem
CCDN.exists_origin_multiplicity
{K : Type u_1}
{σ : Type u_2}
[Field K]
(f : MvPolynomial σ K)
(hf : f ≠ 0)
(hz : (MvPolynomial.eval 0) f = 0)
:
∃ (μ : ℕ),
0 < μ ∧ μ ≤ f.totalDegree ∧ f ∈ MvPolynomial.idealOfVars σ K ^ μ ∧ (MvPolynomial.homogeneousComponent μ) f ≠ 0
The first nonzero homogeneous component realizes the order at the origin.
theorem
CCDN.linear_eval₂_totalDegree_le
{R : Type u_1}
{S : Type u_2}
{σ : Type u_3}
{τ : Type u_4}
[CommRing R]
[CommRing S]
(φ : R →+* S)
(g : σ → MvPolynomial τ S)
(hg : ∀ (j : σ), (g j).totalDegree ≤ 1)
(f : MvPolynomial σ R)
:
Substituting affine linear polynomials does not increase total degree.
theorem
CCDN.exists_hypersurface_reduction_multiplicity
{p : ℕ}
[Fact (Nat.Prime p)]
{σ : Type u_1}
(f : MvPolynomial σ ℤ)
(a : σ → ℤ)
(hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0)
(ha : MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : σ) => ↑(a j)) f = 0)
:
∃ (μ : ℕ),
0 < μ ∧ μ ≤ f.totalDegree ∧ (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) f) ∈ MvPolynomial.idealOfVars σ (ZMod p) ^ μ ∧ (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) f)) ≠ 0
A reduced hypersurface point determines a positive, degree-bounded multiplicity in every ambient dimension.