The infinity ideal is homogeneous, so its geometric zero locus is closed under scalar multiplication. This allows normalization into finite charts.
theorem
CCDN.homogeneous_aeval_scale
{K : Type u_1}
{L : Type u_2}
{σ : Type u_3}
[Field K]
[Field L]
[Algebra K L]
[Finite σ]
(f : MvPolynomial σ K)
{m : ℕ}
(hf : f.IsHomogeneous m)
(z : σ → L)
(c : L)
:
A homogeneous polynomial of degree m satisfies f (c • z) = c ^ m * f z.
theorem
CCDN.infinity_zeroLocus_scale
{K : Type u_1}
{L : Type u_2}
{σ : Type u_3}
[Field K]
[Field L]
[Algebra K L]
[Finite σ]
(I : Ideal (MvPolynomial σ K))
(z : σ → L)
(hz : z ∈ MvPolynomial.zeroLocus L (leadingInfinityIdeal I))
(c : L)
:
The zero locus of the ideal at infinity is a cone: it is stable under scaling by any c.