theorem Thm1324.eval_dehomogenize_eq_general {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) (g : MvPolynomial (Fin (n + 1)) k) (P : Fin n → k) : (MvPolynomial.eval P) ((AffineParts.dehomogenize k i) g) = (MvPolynomial.eval (i.insertNth 1 P)) g

Evaluation–dehomogenization compatibility: for any index $i$, evaluating the dehomogenization of a polynomial $g \in k[X_0, \dots, X_n]$ at an affine point $P \in k^n$ equals evaluating $g$ itself at the projective representative $(P_0, \dots, P_{i-1}, 1, P_i, \dots, P_{n-1})$ obtained by inserting $1$ in the $i$-th coordinate.

theorem Thm1324.eval_dehomogenize_eq {n : ℕ} (k : Type u_1) [Field k] (g : MvPolynomial (Fin (n + 1)) k) (P : Fin n → k) : (MvPolynomial.eval P) ((AffineParts.dehomogenize k 0) g) = (MvPolynomial.eval (Fin.insertNth 0 1 P)) g

Specialization of eval_dehomogenize_eq_general to the standard affine chart $i = 0$: evaluating the dehomogenization at $X_0 = 1$ of $g$ at $P$ equals evaluating $g$ at $(1, P)$.

theorem Thm1324.dehomogenize_surjective {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) : Function.Surjective ⇑(AffineParts.dehomogenize k i)

The dehomogenization ring map $k[X_0, \dots, X_n] \twoheadrightarrow k[Y_1, \dots, Y_n]$ that sets $X_i = 1$ is surjective: every polynomial in the affine chart variables lifts to a polynomial in the projective variables.

theorem Thm1324.dehomogenizedIdeal_isPrime {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) [hI : I.IsPrime] (i : Fin (n + 1)) (hker : RingHom.ker (AffineParts.dehomogenize k i) ≤ I) : (Ideal.map (AffineParts.dehomogenize k i) I).IsPrime

The dehomogenization of a prime ideal is prime, provided the kernel of the dehomogenization map is contained in $I$. This is the ideal-theoretic content of passing from a projective prime ideal to its affine part.

theorem Thm1324.projective_closure_of_affinePart_eq {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) (i : Fin (n + 1)) : {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (i.insertNth 1 P)) f = 0} = {P : Fin n → k | ∀ h ∈ Ideal.map (AffineParts.dehomogenize k i) I, (MvPolynomial.eval P) h = 0}

Set-theoretic identification of the affine part of the zero locus of $I$ (in the chart $X_i = 1$) with the zero locus of the dehomogenized ideal $I \cdot k[\text{affine vars}]$: $\{P : f(\dots,1,\dots,P) = 0 \text{ for all } f \in I\} = \{P : h(P) = 0 \text{ for all } h \in \mathrm{dehom}_i(I)\}$.

theorem Thm1324.theorem_13_24 {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) [hI : I.IsPrime] (i : Fin (n + 1)) (hker : RingHom.ker (AffineParts.dehomogenize k i) ≤ I) : (Ideal.map (AffineParts.dehomogenize k i) I).IsPrime ∧ {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (i.insertNth 1 P)) f = 0} = {P : Fin n → k | ∀ h ∈ Ideal.map (AffineParts.dehomogenize k i) I, (MvPolynomial.eval P) h = 0} ∧ {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0} = {P : Fin n → k | ∀ g ∈ ProjectiveClosure.homogenizeIdeal (Ideal.map (AffineParts.dehomogenize k 0) I), (MvPolynomial.eval (Fin.insertNth 0 1 P)) g = 0}

Theorem 13.24: for a prime ideal $I \subseteq k[X_0, \dots, X_n]$ whose dehomogenization kernel lies in $I$, the dehomogenized ideal $\mathrm{dehom}_i(I)$ is prime, its zero set agrees with the affine part of $V(I)$ in the chart $X_i = 1$, and re-homogenizing recovers the projective closure: $V(I) \cap \{X_0 = 1\} = V(\mathrm{hom}(\mathrm{dehom}_0 I))$. This packages the affine–projective correspondence on prime ideals.

theorem Thm1324Geometric.projectiveVanishingIdeal_isPrime_of_irreducible {n : ℕ} (k : Type u_1) [Field k] (V : Set (Projectivization k (Fin (n + 1) → k))) (hV : ProjectiveVarietyDef.IsProjectiveVariety k V) : (ProjectiveVanishingIdeal.projectiveVanishingIdeal k V).IsPrime

The projective vanishing ideal $I(V)$ of an irreducible (projective) variety $V$ is prime: if $fg \in I(V)$ then $f \in I(V)$ or $g \in I(V)$, reflecting the irreducibility of $V$.

theorem Thm1324Geometric.vanishingIdeal_affine_part_isPrime {n : ℕ} (k : Type u_1) [Field k] (V : Set (Projectivization k (Fin (n + 1) → k))) (hV : ProjectiveVarietyDef.IsProjectiveVariety k V) (i : Fin (n + 1)) (hne : (AffineParts.affinePartZeroLocus k (↑(ProjectiveVanishingIdeal.projectiveVanishingIdeal k V)) i).Nonempty) : (MvPolynomial.vanishingIdeal k (AffineParts.affinePartZeroLocus k (↑(ProjectiveVanishingIdeal.projectiveVanishingIdeal k V)) i)).IsPrime

Geometric form of Theorem 13.24: if $V \subseteq \mathbb{P}^n_k$ is a projective variety and its affine part in the chart $X_i = 1$ is nonempty, then the affine vanishing ideal of that affine part is prime, exhibiting the affine part as an affine variety.