The filtered homogeneous coordinate algebra

For an affine coordinate ideal I, this constructs the subalgebra of (K[x]/I)[w] whose coefficient of w^n is represented by a polynomial of degree at most n. Its homogeneous pieces recover the filtered Hilbert function. Multiplication by the homogenizing coordinate identifies the previous filtered space inside the next piece.

theorem CCDN.filteredCoordinateSpace_algebraMap_mem {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (n : ℕ) (c : K) : (algebraMap K (MvPolynomial σ K ⧸ I)) c ∈ filteredCoordinateSpace I n

Constants lie in every piece of the degree filtration of the coordinate ring.

def CCDN.projectiveCoordinateAlgebra {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) : Subalgebra K (Polynomial (MvPolynomial σ K ⧸ I))

Homogeneous coordinate algebra of the filtered affine coordinate ring.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.projective_monomial_mem {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (n : ℕ) (a : MvPolynomial σ K ⧸ I) : (Polynomial.monomial n) a ∈ projectiveCoordinateAlgebra I ↔ a ∈ filteredCoordinateSpace I n

The monomial a * w ^ n lies in the homogeneous coordinate algebra if and only if a lies in the degree-n piece of the filtered coordinate ring.

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

The homogenizing coordinate w in the homogeneous coordinate algebra.

Equations

• CCDN.projectiveInfinityCoordinate I = ⟨Polynomial.X, ⋯⟩