The prime affine-chart ideal and the transport of projective points and Hilbert degree to that ideal.

theorem CCDN.affineChart_mem_coordinate_kernel_iff {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) (hq : Function.Injective ⇑q) (h0 : q ((Ideal.Quotient.mk I) (MvPolynomial.X 0)) ≠ 0) (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous M) : (affineChart n) f ∈ RingHom.ker (projectiveChartCoordinateMap I q) ↔ f ∈ I

Let q embed the coordinate ring of I into a field with q X₀ ≠ 0. A homogeneous polynomial f lies in I if and only if its dehomogenization affineChart n f lies in the kernel of the coordinate-ratio map projectiveChartCoordinateMap I q.

theorem CCDN.coordinate_kernel_mem_iff_homogenize {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) (hq : Function.Injective ⇑q) (h0 : q ((Ideal.Quotient.mk I) (MvPolynomial.X 0)) ≠ 0) (f : MvPolynomial (Fin n) K) (hf : f.totalDegree ≤ M) : f ∈ RingHom.ker (projectiveChartCoordinateMap I q) ↔ scaledHomogenize M 1 f ∈ I

Let q embed the coordinate ring of I into a field with q X₀ ≠ 0. A polynomial f of total degree at most M lies in the kernel of the coordinate-ratio map projectiveChartCoordinateMap I q if and only if its degree-M homogenization lies in I.

noncomputable def CCDN.projectiveChartIdeal {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) [I.IsPrime] : Ideal (MvPolynomial (Fin n) K)

The ideal of the standard affine chart X₀ ≠ 0 of the projective variety cut out by a homogeneous prime ideal I: the polynomials in the affine coordinates vanishing at the ratios Xⱼ / X₀ in the fraction field of the coordinate ring of I.

Equations

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

instance CCDN.projectiveChartIdeal_isPrime {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) [I.IsPrime] : (projectiveChartIdeal I).IsPrime

theorem CCDN.projectiveChartIdeal_degree {n d : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) [I.IsPrime] (hX : MvPolynomial.X 0 ∉ I) (hdegree : HasProjectiveCurveDegree I d) : HasAffineCurveDegree (projectiveChartIdeal I) d

If a prime ideal I not containing X 0 defines a projective curve of degree d, then its standard affine chart ideal defines an affine curve of degree d.

theorem CCDN.projectiveChartIdeal_point {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) [I.IsPrime] (hX : MvPolynomial.X 0 ∉ I) (x : ProjectivePoint n) (hx : x ∈ projectiveIdealZeroLocus I) (hx0 : Projectivization.rep x 0 ≠ 0) : projectiveAffineCoordinates x ∈ idealZeroLocus (projectiveChartIdeal I)

If a projective point x on the zero locus of a prime ideal I (with X 0 ∉ I) has nonzero first coordinate, then its affine coordinates lie on the zero locus of the standard affine chart ideal of I.