def IsSetOfHomogeneousPolynomials {k : Type u_1} [Field k] {σ : Type u_3} (S : Set (MvPolynomial σ k)) : Prop

A set of multivariate polynomials over k is a set of homogeneous polynomials if every member is homogeneous of some degree.

def projectiveZeroLocus {σ : Type u_3} (k : Type u_4) [Field k] (K : Type u_5) [Field K] [Algebra k K] (S : Set (MvPolynomial σ k)) : Set (Projectivization K (σ → K))

The projective zero locus over K of a set S of k-polynomials: the set of points in ℙ(σ → K) whose representative satisfies p = 0 for every p ∈ S.

@[simp]

theorem mem_projectiveZeroLocus_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} (S : Set (MvPolynomial σ k)) (P : Projectivization K (σ → K)) : P ∈ projectiveZeroLocus k K S ↔ ∀ p ∈ S, (MvPolynomial.aeval P.rep) p = 0

Membership in the projective zero locus unfolds to: every polynomial in S vanishes on a representative of P.

def IsProjectiveAlgebraicSet {K : Type u_2} [Field K] {σ : Type u_3} (k : Type u_4) [Field k] [Algebra k K] (V : Set (Projectivization K (σ → K))) : Prop

A subset V of projective space is a projective algebraic set (defined over k) if it is the projective zero locus of some set of homogeneous k-polynomials.

def IsIrreducibleProjectiveAlgebraicSet {K : Type u_2} [Field K] {σ : Type u_3} (k : Type u_4) [Field k] [Algebra k K] (V : Set (Projectivization K (σ → K))) : Prop

A nonempty projective algebraic set is irreducible (as an algebraic set over k) if it cannot be expressed as a proper union of two projective algebraic sets.

def IsProjectiveVariety {K : Type u_2} [Field K] {σ : Type u_3} (k : Type u_4) [Field k] [Algebra k K] (V : Set (Projectivization K (σ → K))) : Prop

A projective variety over k is an irreducible projective algebraic set defined over k.