Vanishing only at the origin on the infinity section supplies balanced coordinate-power reductions. The Nullstellensatz is used on the kernel of the map to the infinity quotient, over any algebraically closed extension.

noncomputable def CCDN.infinityCoordinateMap {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) : MvPolynomial σ K →ₐ[K] ↥(projectiveCoordinateAlgebra I) ⧸ projectiveInfinityIdeal I

The map from the polynomial ring to the coordinate ring of the section at infinity of the projective closure of I: a polynomial f goes to the class of its radial scaling ∑ n, f_n t ^ n in the homogeneous coordinate algebra modulo the infinity ideal.

Equations

• CCDN.infinityCoordinateMap I = (Ideal.Quotient.mkₐ K (CCDN.projectiveInfinityIdeal I)).comp (CCDN.quotientRadialMap I)

noncomputable def CCDN.leadingInfinityIdeal {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) : Ideal (MvPolynomial σ K)

The homogeneous ideal of the section at infinity of the projective closure of I, defined as the kernel of infinityCoordinateMap I.

Equations

• CCDN.leadingInfinityIdeal I = RingHom.ker (CCDN.infinityCoordinateMap I)

theorem CCDN.leadingInfinityIdeal_component_mem {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (f : MvPolynomial σ K) (hf : f ∈ leadingInfinityIdeal I) (n : ℕ) : (Ideal.Quotient.mk I) ((MvPolynomial.homogeneousComponent (n + 1)) f) ∈ filteredCoordinateSpace I n

If f lies in the ideal at infinity of I, then modulo I each homogeneous component of f of degree n + 1 lies in the filtration piece of degree at most n.

theorem CCDN.exists_power_reductions_of_infinity_avoidance {K : Type u_1} {L : Type u_2} {σ : Type u_3} [Field K] [Field L] [Algebra K L] [IsAlgClosed L] [Finite σ] (I : Ideal (MvPolynomial σ K)) (l : MvPolynomial σ K) (hl : l.IsHomogeneous 1) (hzero : ∀ z ∈ MvPolynomial.zeroLocus L (leadingInfinityIdeal I ⊔ Ideal.span {l}), z = 0) : ∃ (N : ℕ), 0 < N ∧ ∀ (j : σ), ∃ (r : MvPolynomial σ K) (s : MvPolynomial σ K), r.totalDegree ≤ N - 1 ∧ s.totalDegree ≤ N - 1 ∧ (Ideal.Quotient.mk I) (MvPolynomial.X j ^ N) = (Ideal.Quotient.mk I) r + (Ideal.Quotient.mk I) l * (Ideal.Quotient.mk I) s

Avoiding every nonzero infinity direction supplies all coordinate-power reductions with a single positive exponent.