The affine chart of a projective coordinate domain, constructed from coordinate ratios in a field. Its filtered Hilbert function agrees exactly with the homogeneous Hilbert function before dehomogenization.

theorem CCDN.homogeneous_aeval_smul {K : Type u_1} {F : Type u_2} {σ : Type u_3} [Field K] [Field F] [Algebra K F] {f : MvPolynomial σ K} {d : ℕ} (hf : f.IsHomogeneous d) (a : F) (v : σ → F) : (MvPolynomial.aeval (a • v)) f = a ^ d * (MvPolynomial.aeval v) f

A homogeneous polynomial of degree d satisfies f(a • v) = a ^ d * f(v) for evaluations in any field F that is a K-algebra.

noncomputable def CCDN.projectiveChartCoordinateMap {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (q : MvPolynomial (Fin (n + 1)) K ⧸ I →ₐ[K] F) : MvPolynomial (Fin n) K →ₐ[K] F

Given a K-algebra map q from the coordinate ring of I to a field F, the K-algebra map from polynomials in the affine coordinates to F sending Xⱼ to the ratio q Xⱼ₊₁ / q X₀.

Equations

• CCDN.projectiveChartCoordinateMap I q = MvPolynomial.aeval fun (j : Fin n) => q ((Ideal.Quotient.mk I) (MvPolynomial.X j.succ)) / q ((Ideal.Quotient.mk I) (MvPolynomial.X 0))

theorem CCDN.projectiveChartCoordinateMap_chart {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] {n M : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (q : MvPolynomial (Fin (n + 1)) K ⧸ I →ₐ[K] F) (h0 : q ((Ideal.Quotient.mk I) (MvPolynomial.X 0)) ≠ 0) (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous M) : (projectiveChartCoordinateMap I q) ((affineChart n) f) = (q ((Ideal.Quotient.mk I) (MvPolynomial.X 0)))⁻¹ ^ M * q ((Ideal.Quotient.mk I) f)

When q X₀ ≠ 0, the coordinate-ratio map sends the dehomogenization of a homogeneous polynomial f of degree M to (q X₀)⁻¹ ^ M * q f.

theorem CCDN.projective_chart_filtered_finrank {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (q : MvPolynomial (Fin (n + 1)) K ⧸ I →ₐ[K] F) (hq : Function.Injective ⇑q) (h0 : q ((Ideal.Quotient.mk I) (MvPolynomial.X 0)) ≠ 0) (M : ℕ) : Module.finrank K ↥(filteredCoordinateSpace (RingHom.ker (projectiveChartCoordinateMap I q)) M) = projectiveHilbertFunction I M

Let q embed the coordinate ring of I into a field with q X₀ ≠ 0. In every degree M, the filtered Hilbert function of the kernel of the coordinate-ratio map projectiveChartCoordinateMap I q equals the homogeneous Hilbert function of I.

theorem CCDN.projective_chart_degree {F : Type u_1} [Field F] [Algebra ℚ F] {n d : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) (q : MvPolynomial (Fin (n + 1)) ℚ ⧸ I →ₐ[ℚ] F) (hq : Function.Injective ⇑q) (h0 : q ((Ideal.Quotient.mk I) (MvPolynomial.X 0)) ≠ 0) (hdegree : HasProjectiveCurveDegree I d) : HasAffineCurveDegree (RingHom.ker (projectiveChartCoordinateMap I q)) d

Let q embed the coordinate ring of I into a field with q X₀ ≠ 0. If I defines a projective curve of degree d, then the kernel of the coordinate-ratio map projectiveChartCoordinateMap I q defines an affine curve of degree d.