noncomputable def embedPolyLeft (k : Type u_1) [Field k] (m n : ℕ) : MvPolynomial (Fin m) (AlgebraicClosure k) →ₐ[AlgebraicClosure k] MvPolynomial (Fin (m + n)) (AlgebraicClosure k)

Embedding $\overline{k}[x_1, \ldots, x_m] \hookrightarrow \overline{k}[x_1, \ldots, x_{m+n}]$ in the first $m$ variables, by renaming via Fin.castAdd.

noncomputable def embedPolyRight (k : Type u_1) [Field k] (m n : ℕ) : MvPolynomial (Fin n) (AlgebraicClosure k) →ₐ[AlgebraicClosure k] MvPolynomial (Fin (m + n)) (AlgebraicClosure k)

Embedding $\overline{k}[y_1, \ldots, y_n] \hookrightarrow \overline{k}[x_1, \ldots, x_{m+n}]$ in the last $n$ variables, by renaming via Fin.natAdd.

def embedSetLeft (k : Type u_1) [Field k] (m n : ℕ) (S : Set (MvPolynomial (Fin m) (AlgebraicClosure k))) : Set (MvPolynomial (Fin (m + n)) (AlgebraicClosure k))

Image of a set of polynomials under embedPolyLeft.

def embedSetRight (k : Type u_1) [Field k] (m n : ℕ) (S : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) : Set (MvPolynomial (Fin (m + n)) (AlgebraicClosure k))

Image of a set of polynomials under embedPolyRight.

def ProductAlgebraicSet (k : Type u_1) [Field k] (m n : ℕ) (S_X : Set (MvPolynomial (Fin m) (AlgebraicClosure k))) (S_Y : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) : Set (AffineSpace_k k (m + n))

Definition 16.2: the product algebraic set $V(S_X) \times V(S_Y) \subseteq \overline{k}^{m+n}$, defined as the algebraic set in $\overline{k}^{m+n}$ cut out by the embedded polynomials.

def projLeft (k : Type u_1) [Field k] (m n : ℕ) (P : AffineSpace_k k (m + n)) : AffineSpace_k k m

Projection $\overline{k}^{m+n} \to \overline{k}^m$ onto the first $m$ coordinates.

def projRight (k : Type u_1) [Field k] (m n : ℕ) (P : AffineSpace_k k (m + n)) : AffineSpace_k k n

Projection $\overline{k}^{m+n} \to \overline{k}^n$ onto the last $n$ coordinates.

def CartesianProduct (k : Type u_1) [Field k] (m n : ℕ) (X : Set (AffineSpace_k k m)) (Y : Set (AffineSpace_k k n)) : Set (AffineSpace_k k (m + n))

The Cartesian product $X \times Y \subseteq \overline{k}^{m+n}$ as a set, defined by the projection criteria.

@[simp]

theorem projLeft_append (k : Type u_1) [Field k] (m n : ℕ) (a : AffineSpace_k k m) (b : AffineSpace_k k n) : projLeft k m n (Fin.append a b) = a

Projecting Fin.append a b to the left gives a.

@[simp]

theorem projRight_append (k : Type u_1) [Field k] (m n : ℕ) (a : AffineSpace_k k m) (b : AffineSpace_k k n) : projRight k m n (Fin.append a b) = b

Projecting Fin.append a b to the right gives b.

theorem append_proj (k : Type u_1) [Field k] (m n : ℕ) (P : AffineSpace_k k (m + n)) : Fin.append (projLeft k m n P) (projRight k m n P) = P

Reconstruction: appending the left and right projections of $P$ recovers $P$.

theorem mem_productAlgebraicSet (k : Type u_1) [Field k] (m n : ℕ) (S_X : Set (MvPolynomial (Fin m) (AlgebraicClosure k))) (S_Y : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) (P : AffineSpace_k k (m + n)) : P ∈ ProductAlgebraicSet k m n S_X S_Y ↔ projLeft k m n P ∈ AlgebraicSet k m S_X ∧ projRight k m n P ∈ AlgebraicSet k n S_Y

A point $P \in \overline{k}^{m+n}$ lies in $V(S_X) \times V(S_Y)$ iff its left projection lies in $V(S_X)$ and its right projection lies in $V(S_Y)$.

theorem productAlgebraicSet_nonempty (k : Type u_1) [Field k] (m n : ℕ) (S_X : Set (MvPolynomial (Fin m) (AlgebraicClosure k))) (S_Y : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) (hX : (AlgebraicSet k m S_X).Nonempty) (hY : (AlgebraicSet k n S_Y).Nonempty) : (ProductAlgebraicSet k m n S_X S_Y).Nonempty

The product of two nonempty algebraic sets is nonempty.

noncomputable def partialEvalRight (k : Type u_1) [Field k] (m n : ℕ) (b : AffineSpace_k k n) : MvPolynomial (Fin (m + n)) (AlgebraicClosure k) →+* MvPolynomial (Fin m) (AlgebraicClosure k)

Partial evaluation of a polynomial in $m+n$ variables by fixing the last $n$ variables to the values $b \in \overline{k}^n$, returning a polynomial in the first $m$ variables.

theorem eval_partialEvalRight (k : Type u_1) [Field k] (m n : ℕ) (b : AffineSpace_k k n) (f : MvPolynomial (Fin (m + n)) (AlgebraicClosure k)) (a : AffineSpace_k k m) : (MvPolynomial.eval a) ((partialEvalRight k m n b) f) = (MvPolynomial.eval (Fin.append a b)) f

Compatibility: evaluating partialEvalRight b f at a equals evaluating f at the appended point Fin.append a b.

theorem algebraicSubset_fiber_left (k : Type u_1) [Field k] (m n : ℕ) (T : Set (MvPolynomial (Fin (m + n)) (AlgebraicClosure k))) (b : AffineSpace_k k n) : IsAlgebraicSubset k m {a : AffineSpace_k k m | Fin.append a b ∈ AlgebraicSet k (m + n) T}

For an algebraic set $V(T) \subseteq \overline{k}^{m+n}$, the fiber $\{a \mid (a, b) \in V(T)\}$ over a fixed $b \in \overline{k}^n$ is an algebraic subset of $\overline{k}^m$.

noncomputable def partialEvalLeft (k : Type u_1) [Field k] (m n : ℕ) (a : AffineSpace_k k m) : MvPolynomial (Fin (m + n)) (AlgebraicClosure k) →+* MvPolynomial (Fin n) (AlgebraicClosure k)

Partial evaluation of a polynomial in $m+n$ variables by fixing the first $m$ variables to the values $a \in \overline{k}^m$, returning a polynomial in the last $n$ variables.

theorem eval_partialEvalLeft (k : Type u_1) [Field k] (m n : ℕ) (a : AffineSpace_k k m) (f : MvPolynomial (Fin (m + n)) (AlgebraicClosure k)) (b : AffineSpace_k k n) : (MvPolynomial.eval b) ((partialEvalLeft k m n a) f) = (MvPolynomial.eval (Fin.append a b)) f

Compatibility: evaluating partialEvalLeft a f at b equals evaluating f at Fin.append a b.

theorem algebraicSubset_fiber_right (k : Type u_1) [Field k] (m n : ℕ) (T : Set (MvPolynomial (Fin (m + n)) (AlgebraicClosure k))) (a : AffineSpace_k k m) : IsAlgebraicSubset k n {b : AffineSpace_k k n | Fin.append a b ∈ AlgebraicSet k (m + n) T}

For an algebraic set $V(T) \subseteq \overline{k}^{m+n}$, the fiber $\{b \mid (a, b) \in V(T)\}$ over a fixed $a \in \overline{k}^m$ is an algebraic subset of $\overline{k}^n$.

theorem isAlgebraicSubset_iInter (k : Type u_1) [Field k] {ι : Type u_2} (n : ℕ) (V : ι → Set (AffineSpace_k k n)) (hV : ∀ (i : ι), IsAlgebraicSubset k n (V i)) : IsAlgebraicSubset k n (⋂ (i : ι), V i)

An arbitrary intersection of algebraic subsets is an algebraic subset (cut out by the union of the defining polynomial sets).

theorem productVariety (k : Type u_1) [Field k] (m n : ℕ) (S_X : Set (MvPolynomial (Fin m) (AlgebraicClosure k))) (S_Y : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) (hX : IsIrreducibleAlgebraicSet k m (AlgebraicSet k m S_X)) (hY : IsIrreducibleAlgebraicSet k n (AlgebraicSet k n S_Y)) : IsIrreducibleAlgebraicSet k (m + n) (ProductAlgebraicSet k m n S_X S_Y)

Lemma 16.4/16.5: the product of two irreducible affine algebraic sets is irreducible (the product of two affine varieties is again an affine variety).

def vanishingIdeal_kbar (k : Type u_1) [Field k] (n : ℕ) (V : Set (AffineSpace_k k n)) : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k))

The $\overline{k}$-vanishing ideal of a subset $V \subseteq \overline{k}^n$: polynomials in $\overline{k}[x_1, \ldots, x_n]$ that vanish on $V$.

theorem subset_vanishingIdeal_algebraicSet (k : Type u_1) [Field k] (n : ℕ) (S : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) : S ⊆ ↑(vanishingIdeal_kbar k n (AlgebraicSet k n S))

$S \subseteq I(V(S))$: every polynomial in $S$ vanishes on its own zero set.

theorem algebraicSet_anti (k : Type u_1) [Field k] (n : ℕ) {S T : Set (MvPolynomial (Fin n) (AlgebraicClosure k))} (h : S ⊆ T) : AlgebraicSet k n T ⊆ AlgebraicSet k n S

The algebraic set operator is antitone: $S \subseteq T$ implies $V(T) \subseteq V(S)$.

theorem subset_algebraicSet_vanishingIdeal (k : Type u_1) [Field k] (n : ℕ) (V : Set (AffineSpace_k k n)) : V ⊆ AlgebraicSet k n ↑(vanishingIdeal_kbar k n V)

$V \subseteq V(I(V))$: every point of $V$ lies in the zero set of its vanishing ideal.

theorem algebraicSet_vanishingIdeal_eq (k : Type u_1) [Field k] (n : ℕ) (S : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) : AlgebraicSet k n ↑(vanishingIdeal_kbar k n (AlgebraicSet k n S)) = AlgebraicSet k n S

Closure-like idempotence: $V(I(V(S))) = V(S)$.

theorem vanishingIdeal_kbar_anti (k : Type u_1) [Field k] (n : ℕ) {V W : Set (AffineSpace_k k n)} (h : V ⊆ W) : vanishingIdeal_kbar k n W ≤ vanishingIdeal_kbar k n V

The vanishing ideal operator is antitone in the subset argument.

theorem vanishingIdeal_kbar_injective_on_algebraicSets (k : Type u_1) [Field k] (n : ℕ) {S₁ S₂ : Set (MvPolynomial (Fin n) (AlgebraicClosure k))} (heq : vanishingIdeal_kbar k n (AlgebraicSet k n S₁) = vanishingIdeal_kbar k n (AlgebraicSet k n S₂)) : AlgebraicSet k n S₁ = AlgebraicSet k n S₂

The vanishing ideal operator is injective on algebraic sets: equal ideals implies equal algebraic sets.

theorem vanishingIdeal_kbar_strictAnti_algebraicSets (k : Type u_1) [Field k] (n : ℕ) {S₁ S₂ : Set (MvPolynomial (Fin n) (AlgebraicClosure k))} (h : AlgebraicSet k n S₁ ⊂ AlgebraicSet k n S₂) : vanishingIdeal_kbar k n (AlgebraicSet k n S₂) < vanishingIdeal_kbar k n (AlgebraicSet k n S₁)

Strict antitone: a proper inclusion of algebraic sets gives a strict inclusion of vanishing ideals (in the reverse direction).

theorem vanishingIdeal_kbar_injective_closeds (k : Type u_1) [Field k] (n : ℕ) {V₁ V₂ : Set (AffineSpace_k k n)} (hV₁ : IsAlgebraicSetAffine k n V₁) (hV₂ : IsAlgebraicSetAffine k n V₂) (heq : vanishingIdeal_kbar k n V₁ = vanishingIdeal_kbar k n V₂) : V₁ = V₂

The vanishing ideal is injective on Zariski-closed subsets of $\overline{k}^n$.

theorem affineSpace_noetherianSpace (k : Type u_1) [Field k] (n : ℕ) : TopologicalSpace.NoetherianSpace (AffineSpace_k k n)

Affine space $\overline{k}^n$ equipped with the Zariski topology is a Noetherian topological space (consequence of the Hilbert basis theorem).

theorem affineSpace_quasiCompact (k : Type u_1) [Field k] (n : ℕ) (S : Set (AffineSpace_k k n)) : IsCompact S

Every subset of $\overline{k}^n$ (with the Zariski topology) is quasi-compact, a consequence of $\overline{k}^n$ being Noetherian.

theorem idealOfAlgebraicSet_le_ker_eval {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P : AffineSpace_k k n) (hP : P ∈ V) : idealOfAlgebraicSet V ≤ RingHom.ker (MvPolynomial.eval P)

If $P \in V$, then every polynomial vanishing on $V$ vanishes at $P$, i.e. $I(V) \subseteq \ker(\mathrm{eval}_P)$.

noncomputable def evalOnCoordinateRingBar {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P : AffineSpace_k k n) (hP : P ∈ V) : AffineCoordinateRingBar V →+* AlgebraicClosure k

Evaluation at a point $P \in V$ descends to a ring homomorphism $\overline{k}[V] \to \overline{k}$ from the coordinate ring.

theorem evalOnCoordinateRingBar_mk {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P : AffineSpace_k k n) (hP : P ∈ V) (f : MvPolynomial (Fin n) (AlgebraicClosure k)) : (evalOnCoordinateRingBar V P hP) ((Ideal.Quotient.mk (idealOfAlgebraicSet V)) f) = (MvPolynomial.eval P) f

The descended evaluation commutes with the quotient map: it agrees with eval P on polynomials.

theorem evalOnCoordinateRingBar_surjective {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P : AffineSpace_k k n) (hP : P ∈ V) : Function.Surjective ⇑(evalOnCoordinateRingBar V P hP)

The evaluation map $\overline{k}[V] \to \overline{k}$ at a point of $V$ is surjective.

noncomputable def maximalIdealOfPoint {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P : AffineSpace_k k n) (hP : P ∈ V) : Ideal (AffineCoordinateRingBar V)

The maximal ideal $\mathfrak{m}_P \subseteq \overline{k}[V]$ associated to a point $P \in V$, defined as the kernel of evaluation at $P$.

theorem maximalIdealOfPoint_isMaximal {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P : AffineSpace_k k n) (hP : P ∈ V) : (maximalIdealOfPoint V P hP).IsMaximal

The ideal $\mathfrak{m}_P$ is maximal, since it is the kernel of a surjection onto a field.

theorem comap_maximalIdealOfPoint_eq_ker_eval {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P : AffineSpace_k k n) (hP : P ∈ V) : Ideal.comap (Ideal.Quotient.mk (idealOfAlgebraicSet V)) (maximalIdealOfPoint V P hP) = RingHom.ker (MvPolynomial.eval P)

Pulling back $\mathfrak{m}_P$ along the quotient map recovers the kernel of eval P.

theorem maximalIdealOfPoint_injective {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (P₁ P₂ : AffineSpace_k k n) (hP₁ : P₁ ∈ V) (hP₂ : P₂ ∈ V) (heq : maximalIdealOfPoint V P₁ hP₁ = maximalIdealOfPoint V P₂ hP₂) : P₁ = P₂

The map $P \mapsto \mathfrak{m}_P$ from points of $V$ to maximal ideals of $\overline{k}[V]$ is injective.

theorem idealOfAlgebraicSet_le_vanishingIdeal_singleton_iff {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (hV : IsAlgebraicSubset k n V) (P : AffineSpace_k k n) : idealOfAlgebraicSet V ≤ MvPolynomial.vanishingIdeal (AlgebraicClosure k) {P} ↔ P ∈ V

For an algebraic subset $V$, $I(V) \subseteq I(\{P\})$ iff $P \in V$.

theorem lemma_16_3 {k : Type u_1} [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (hV : IsAlgebraicSubset k n V) : Function.Bijective fun (Pt : ↑V) => ⟨maximalIdealOfPoint V ↑Pt ⋯, ⋯⟩

Lemma 16.3: for an affine algebraic subset $V$, the map $P \mapsto \mathfrak{m}_P$ is a bijection from points of $V$ to maximal ideals of $\overline{k}[V]$.

def ProductProjectiveSpace (k : Type u_2) [Field k] (m n : ℕ) : Type u_2

The product projective space $\mathbb{P}^m \times \mathbb{P}^n$ over $k$ as a Cartesian product of projective spaces.

structure BihomogPoly (k : Type u_2) [Field k] (m n : ℕ) : Type u_2

A bihomogeneous polynomial of bi-degree $(d_X, d_Y)$: a polynomial in $m + 1 + (n + 1)$ variables which is homogeneous of degree $d_X$ in the first $m + 1$ variables and homogeneous of degree $d_Y$ in the last $n + 1$ variables.

• poly : MvPolynomial (Fin (m + 1 + (n + 1))) (AlgebraicClosure k)
• degX : ℕ
• degY : ℕ
• homogX (c : AlgebraicClosure k) (v : Fin (m + 1 + (n + 1)) → AlgebraicClosure k) : (MvPolynomial.eval fun (i : Fin (m + 1 + (n + 1))) => if ↑i < m + 1 then c * v i else v i) self.poly = c ^ self.degX * (MvPolynomial.eval v) self.poly
• homogY (c : AlgebraicClosure k) (v : Fin (m + 1 + (n + 1)) → AlgebraicClosure k) : (MvPolynomial.eval fun (i : Fin (m + 1 + (n + 1))) => if ↑i < m + 1 then v i else c * v i) self.poly = c ^ self.degY * (MvPolynomial.eval v) self.poly

noncomputable def embedHomogPolyLeft {k : Type u_2} [Field k] (m n : ℕ) : MvPolynomial (Fin (m + 1)) (AlgebraicClosure k) →ₐ[AlgebraicClosure k] MvPolynomial (Fin (m + 1 + (n + 1))) (AlgebraicClosure k)

Embedding $\overline{k}[x_0, \ldots, x_m] \hookrightarrow$ the bigger polynomial ring in $m + 1 + (n + 1)$ variables, on the first $m + 1$ variables.

noncomputable def embedHomogPolyRight {k : Type u_2} [Field k] (m n : ℕ) : MvPolynomial (Fin (n + 1)) (AlgebraicClosure k) →ₐ[AlgebraicClosure k] MvPolynomial (Fin (m + 1 + (n + 1))) (AlgebraicClosure k)

Embedding $\overline{k}[y_0, \ldots, y_n] \hookrightarrow$ the bigger polynomial ring in $m + 1 + (n + 1)$ variables, on the last $n + 1$ variables.

def embedHomogSetLeft {k : Type u_2} [Field k] (m n : ℕ) (S : Set (MvPolynomial (Fin (m + 1)) (AlgebraicClosure k))) : Set (MvPolynomial (Fin (m + 1 + (n + 1))) (AlgebraicClosure k))

Image of a set of homogeneous polynomials under embedHomogPolyLeft.

def embedHomogSetRight {k : Type u_2} [Field k] (m n : ℕ) (S : Set (MvPolynomial (Fin (n + 1)) (AlgebraicClosure k))) : Set (MvPolynomial (Fin (m + 1 + (n + 1))) (AlgebraicClosure k))

Image of a set of homogeneous polynomials under embedHomogPolyRight.

theorem eval_embedHomogPolyLeft {k : Type u_2} [Field k] (m n : ℕ) (p : MvPolynomial (Fin (m + 1)) (AlgebraicClosure k)) (a : Fin (m + 1) → AlgebraicClosure k) (b : Fin (n + 1) → AlgebraicClosure k) : (MvPolynomial.eval (Fin.append a b)) ((embedHomogPolyLeft m n) p) = (MvPolynomial.eval a) p

Evaluating $\mathrm{embedHomogPolyLeft}(p)$ at Fin.append a b equals evaluating $p$ at $a$.

theorem eval_embedHomogPolyRight {k : Type u_2} [Field k] (m n : ℕ) (p : MvPolynomial (Fin (n + 1)) (AlgebraicClosure k)) (a : Fin (m + 1) → AlgebraicClosure k) (b : Fin (n + 1) → AlgebraicClosure k) : (MvPolynomial.eval (Fin.append a b)) ((embedHomogPolyRight m n) p) = (MvPolynomial.eval b) p

Evaluating $\mathrm{embedHomogPolyRight}(p)$ at Fin.append a b equals evaluating $p$ at $b$.

def combinedHomogPolySet {k : Type u_2} [Field k] (m n : ℕ) (S_X : Set (HomogPoly k m)) (S_Y : Set (HomogPoly k n)) : Set (MvPolynomial (Fin (m + 1 + (n + 1))) (AlgebraicClosure k))

The combined polynomial set: union of the embeddings of homogeneous polynomial sets from $\mathbb{P}^m$ and $\mathbb{P}^n$ into the bigger polynomial ring.

theorem combinedHomogPolySet_vanish_of_rescale {k : Type u_2} [Field k] {m n : ℕ} {S_X : Set (HomogPoly k m)} {S_Y : Set (HomogPoly k n)} {a₁ : Fin (m + 1) → AlgebraicClosure k} {b₁ : Fin (n + 1) → AlgebraicClosure k} {a₂ : Fin (m + 1) → AlgebraicClosure k} {b₂ : Fin (n + 1) → AlgebraicClosure k} {c d : AlgebraicClosure k} (hc : c ≠ 0) (hd : d ≠ 0) (ha : a₁ = fun (i : Fin (m + 1)) => c * a₂ i) (hb : b₁ = fun (i : Fin (n + 1)) => d * b₂ i) (h : ∀ f ∈ combinedHomogPolySet m n S_X S_Y, (MvPolynomial.eval (Fin.append a₁ b₁)) f = 0) (f : MvPolynomial (Fin (m + 1 + (n + 1))) (AlgebraicClosure k)) : f ∈ combinedHomogPolySet m n S_X S_Y → (MvPolynomial.eval (Fin.append a₂ b₂)) f = 0

Vanishing of the combined homogeneous polynomial set is invariant under rescaling each of the two homogeneous coordinate vectors by a nonzero scalar (well-definedness on projective coordinates).

def ProductProjectiveAlgebraicSet {k : Type u_2} [Field k] (m n : ℕ) (S_X : Set (HomogPoly k m)) (S_Y : Set (HomogPoly k n)) : Set (ProductProjectiveSpace k m n)

The product projective algebraic set in $\mathbb{P}^m \times \mathbb{P}^n$ cut out by two sets of homogeneous polynomials, defined as the common zero locus of the combined set on the quotient $\mathbb{P}^m \times \mathbb{P}^n$.

def IsProductProjectiveAlgSet {k : Type u_2} [Field k] (m n : ℕ) (V : Set (ProductProjectiveSpace k m n)) : Prop

A subset $V \subseteq \mathbb{P}^m \times \mathbb{P}^n$ is a product projective algebraic set if it equals ProductProjectiveAlgebraicSet S_X S_Y for some homogeneous polynomial sets.

theorem mem_productProjectiveAlgebraicSet {k : Type u_2} [Field k] (m n : ℕ) (S_X : Set (HomogPoly k m)) (S_Y : Set (HomogPoly k n)) (PQ : ProductProjectiveSpace k m n) : PQ ∈ ProductProjectiveAlgebraicSet m n S_X S_Y ↔ PQ.1 ∈ ProjVanishingSet k m S_X ∧ PQ.2 ∈ ProjVanishingSet k n S_Y

A point $(P, Q) \in \mathbb{P}^m \times \mathbb{P}^n$ lies in the product projective algebraic set iff $P$ lies in the projective vanishing set of $S_X$ and $Q$ lies in the projective vanishing set of $S_Y$.

def concatVec {k : Type u_2} [Field k] (m n : ℕ) (a : Fin (m + 1) → AlgebraicClosure k) (b : Fin (n + 1) → AlgebraicClosure k) : Fin (m + 1 + (n + 1)) → AlgebraicClosure k

Concatenation of two vectors of homogeneous coordinates from $\mathbb{A}^{m+1}$ and $\mathbb{A}^{n+1}$ into a single vector in $\mathbb{A}^{m+1+(n+1)}$.

noncomputable def segreMap {k : Type u_2} [Field k] (m n : ℕ) (a : Fin (m + 1) → AlgebraicClosure k) (b : Fin (n + 1) → AlgebraicClosure k) : Fin ((m + 1) * (n + 1)) → AlgebraicClosure k

The Segre map on coordinates: $((a_i), (b_j)) \mapsto (a_i b_j)_{i,j}$, sending $\mathbb{A}^{m+1} \times \mathbb{A}^{n+1} \to \mathbb{A}^{(m+1)(n+1)}$, indexed by the pair $(i, j)$ encoded as $i \cdot (n+1) + j$.