noncomputable def segreMap (k : Type u_1) [CommRing k] : MvPolynomial (Fin 4) k →ₐ[k] MvPolynomial (Fin 4) k

Algebra map underlying the Segre embedding ℙ¹ × ℙ¹ → ℙ³: sends the coordinates (z₀, z₁, z₂, z₃) of ℙ³ to the bilinear monomials (x₀y₀, x₀y₁, x₁y₀, x₁y₁) in the coordinates of ℙ¹ × ℙ¹.

noncomputable def segreRelation (k : Type u_1) [CommRing k] : MvPolynomial (Fin 4) k

Defining relation of the Segre quadric in ℙ³: z₀ z₃ − z₁ z₂.

theorem segre_relation_in_kernel (k : Type u_1) [CommRing k] : (segreMap k) (segreRelation k) = 0

The Segre relation z₀ z₃ − z₁ z₂ lies in the kernel of the Segre embedding: pulling it back along segreMap gives zero.

theorem segre_algebraic_identity {R : Type u_1} [CommRing R] (x₀ x₁ y₀ y₁ : R) : x₀ * y₀ * (x₁ * y₁) - x₀ * y₁ * (x₁ * y₀) = 0

Polynomial identity behind the Segre relation: (x₀ y₀)(x₁ y₁) − (x₀ y₁)(x₁ y₀) = 0 in any commutative ring.