Exact homogeneous Hilbert functions of a principal equation. Multiplication by a homogeneous nonzero equation identifies the entire homogeneous kernel.
theorem
CCDN.homogeneous_multiplier
{K : Type u_1}
{σ : Type u_2}
[CommRing K]
[IsDomain K]
{f u : MvPolynomial σ K}
{d M : ℕ}
(hf : f.IsHomogeneous d)
(hf0 : f ≠ 0)
(hfu : (f * u).IsHomogeneous M)
(hM : d ≤ M)
:
u.IsHomogeneous (M - d)
If f ≠ 0 is homogeneous of degree d and f * u is homogeneous of degree M ≥ d, then u
is homogeneous of degree M - d.
noncomputable def
CCDN.homogeneousCoordinateSpace
{K : Type u_1}
{σ : Type u_2}
[Field K]
(I : Ideal (MvPolynomial σ K))
(M : ℕ)
:
Submodule K (MvPolynomial σ K ⧸ I)
The degree-M part of the graded coordinate ring: the image of the homogeneous polynomials of
degree M in K[X] ⧸ I.
Equations
Instances For
noncomputable def
CCDN.homogeneousMultiples
{K : Type u_1}
{σ : Type u_2}
[Field K]
(f : MvPolynomial σ K)
(d M : ℕ)
:
Submodule K (MvPolynomial σ K)
The multiples f * u of f by homogeneous polynomials u of degree M - d.
Equations
- CCDN.homogeneousMultiples f d M = Submodule.map (LinearMap.mulLeft K f) (MvPolynomial.homogeneousSubmodule σ K (M - d))
Instances For
theorem
CCDN.homogeneousMultiples_finrank
{K : Type u_1}
{σ : Type u_2}
[Field K]
(f : MvPolynomial σ K)
(hf : f ≠ 0)
(d M : ℕ)
:
Module.finrank K ↥(homogeneousMultiples f d M) = Module.finrank K ↥(MvPolynomial.homogeneousSubmodule σ K (M - d))
For f ≠ 0, the space of homogeneous multiples homogeneousMultiples f d M has the dimension
of the space of homogeneous polynomials of degree M - d.
theorem
CCDN.principal_homogeneous_hilbert_count
{K : Type u_1}
[Field K]
{n d M : ℕ}
(f : MvPolynomial (Fin (n + 1)) K)
(hf : f.IsHomogeneous d)
(hf0 : f ≠ 0)
(hM : d ≤ M)
:
Module.finrank K ↥(homogeneousCoordinateSpace (Ideal.span {f}) M) + (n + (M - d)).choose (M - d) = (n + M).choose M
Exact projective hypersurface Hilbert count, with no geometric hypothesis.