Origin-adic layers of a nonhomogeneous hypersurface. The first nonzero homogeneous part supplies the singular multiplicity bound directly.

theorem CCDN.homogeneous_mem_origin_power {K : Type u_1} {σ : Type u_2} [CommRing K] {f : MvPolynomial σ K} {k : ℕ} (hf : f.IsHomogeneous k) : f ∈ MvPolynomial.idealOfVars σ K ^ k

A homogeneous polynomial of degree k lies in the k-th power of the ideal of the origin.

theorem CCDN.sub_homogeneousComponent_mem_origin_power {K : Type u_1} {σ : Type u_2} [CommRing K] {f : MvPolynomial σ K} {k : ℕ} (hf : f ∈ MvPolynomial.idealOfVars σ K ^ k) : f - (MvPolynomial.homogeneousComponent k) f ∈ MvPolynomial.idealOfVars σ K ^ (k + 1)

Taking the first permitted homogeneous part changes a polynomial only by one higher power of the origin ideal.

noncomputable def CCDN.originTruncationIdeal {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) (k : ℕ) : Ideal (MvPolynomial σ K)

The ideal (f) + 𝔪₀ ^ (k + 1), where 𝔪₀ is the ideal of the origin; the quotient by it is the coordinate ring of f = 0 truncated at the origin.

Equations

• CCDN.originTruncationIdeal f k = Ideal.span {f} ⊔ MvPolynomial.idealOfVars σ K ^ (k + 1)

noncomputable def CCDN.originLayer {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) (k : ℕ) : Submodule K (MvPolynomial σ K ⧸ originTruncationIdeal f k)

The degree-k layer of the ideal of the origin on the hypersurface f = 0: the image of the k-th power of the ideal of the origin in the quotient by (f) and the (k + 1)-th power. This is the image of the ideal power, not a tangent-cone model.

Equations

• CCDN.originLayer f k = Submodule.map (Ideal.Quotient.mkₐ K (CCDN.originTruncationIdeal f k)).toLinearMap (Submodule.restrictScalars K (MvPolynomial.idealOfVars σ K ^ k))

theorem CCDN.originLayer_eq_homogeneousCoordinateSpace {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) (k : ℕ) : originLayer f k = homogeneousCoordinateSpace (originTruncationIdeal f k) k

Homogeneous degree-k polynomials generate the degree-k layer.

theorem CCDN.initial_form_multiple_mem_truncation {K : Type u_1} {σ : Type u_2} [Field K] {f : MvPolynomial σ K} {μ k : ℕ} (hf : f ∈ MvPolynomial.idealOfVars σ K ^ μ) (hk : μ ≤ k) {u : MvPolynomial σ K} (hu : u.IsHomogeneous (k - μ)) : (MvPolynomial.homogeneousComponent μ) f * u ∈ originTruncationIdeal f k

The initial homogeneous equation vanishes in each origin-adic layer after multiplying by an allowed homogeneous polynomial.

theorem CCDN.originLayer_hilbert_bound {K : Type u_1} [Field K] {n μ k : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f ∈ MvPolynomial.idealOfVars (Fin (n + 1)) K ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) f ≠ 0) (hk : μ ≤ k) : Module.finrank K ↥(originLayer f k) + (n + (k - μ)).choose (k - μ) ≤ (n + k).choose k

The first nonzero homogeneous part gives the expected binomial upper bound for the local layer.

instance CCDN.originLayer_finite {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (f : MvPolynomial σ K) (k : ℕ) : Module.Finite K ↥(originLayer f k)

theorem CCDN.originLayer_finrank_le {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (k : ℕ) : Module.finrank K ↥(originLayer f k) ≤ (n + k).choose k

The degree-k origin layer of a hypersurface in n + 1 variables has dimension at most the number (n + k).choose k of monomials of degree k.

theorem CCDN.plane_originLayer_finrank_le_multiplicity {K : Type u_1} [Field K] {μ k : ℕ} (f : MvPolynomial (Fin 2) K) (hf : f ∈ MvPolynomial.idealOfVars (Fin 2) K ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) f ≠ 0) : Module.finrank K ↥(originLayer f k) ≤ μ

In the plane-curve case each origin-adic layer has dimension at most its multiplicity. This is the bound needed for the quadratic local exponent.