The quotient by the infinity coordinate

The degree-n+1 image in the quotient of the filtered homogeneous coordinate algebra by its infinity coordinate has dimension H(n+1)-H(n). Thus the certified affine Hilbert degree is the eventual graded dimension of a quotient ring.

noncomputable def CCDN.projectiveMonomialMap {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (n : ℕ) : ↥(filteredCoordinateSpace I n) →ₗ[K] ↥(projectiveCoordinateAlgebra I)

A homogeneous element with coefficient in the prescribed filtered space.

Equations

• CCDN.projectiveMonomialMap I n = { toFun := fun (a : ↥(CCDN.filteredCoordinateSpace I n)) => ⟨(Polynomial.monomial n) ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CCDN.projectiveMonomialMap_val {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (n : ℕ) (a : ↥(filteredCoordinateSpace I n)) : ↑((projectiveMonomialMap I n) a) = (Polynomial.monomial n) ↑a

projectiveMonomialMap I n a is the monomial a · Tⁿ in the homogeneous coordinate algebra.

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

The ideal cutting out the infinity section in the homogeneous coordinate ring.

Equations

• CCDN.projectiveInfinityIdeal I = Ideal.span {CCDN.projectiveInfinityCoordinate I}

instance CCDN.projectiveInfinityIdeal_twoSided {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) : (projectiveInfinityIdeal I).IsTwoSided

theorem CCDN.projectiveMonomial_mem_infinityIdeal {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (n : ℕ) (a : ↥(filteredCoordinateSpace I (n + 1))) : (projectiveMonomialMap I (n + 1)) a ∈ projectiveInfinityIdeal I ↔ ↑a ∈ filteredCoordinateSpace I n

Divisibility by the new coordinate is exactly membership one step lower in the affine degree filtration.

noncomputable def CCDN.projectivePieceToInfinity {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (n : ℕ) : ↥(filteredCoordinateSpace I (n + 1)) →ₗ[K] ↥(projectiveCoordinateAlgebra I) ⧸ projectiveInfinityIdeal I

Map a homogeneous piece to the quotient by the infinity coordinate.

Equations

• CCDN.projectivePieceToInfinity I n = (Ideal.Quotient.mkₐ K (CCDN.projectiveInfinityIdeal I)).toLinearMap ∘ₗ CCDN.projectiveMonomialMap I (n + 1)

noncomputable def CCDN.infinityGradedSpace {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (n : ℕ) : Submodule K (↥(projectiveCoordinateAlgebra I) ⧸ projectiveInfinityIdeal I)

Degree-n+1 elements of the infinity quotient ring.

Equations

• CCDN.infinityGradedSpace I n = (CCDN.projectivePieceToInfinity I n).range

instance CCDN.infinityGradedSpace_finite {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I : Ideal (MvPolynomial σ K)) (n : ℕ) : Module.Finite K ↥(infinityGradedSpace I n)

theorem CCDN.infinityGradedSpace_eventually_degree {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I : Ideal (MvPolynomial σ K)) {d N : ℕ} {b : ℤ} (hdegree : ∀ n ≥ N, ↑(Module.finrank K ↥(filteredCoordinateSpace I n)) = ↑d * ↑n + b) (n : ℕ) : n ≥ N → Module.finrank K ↥(infinityGradedSpace I n) = d

Every certified affine Hilbert degree is the eventual graded dimension of the quotient by the infinity coordinate.