Zero loci of polynomial families in complex projective space

For a family p : ι → MvPolynomial (Fin N) ℂ, the set complexProjectiveZeroLocus p consists of the complex lines L in ℂ^N, that is the points of Projectivization ℂ (Fin N → ℂ), such that every p i vanishes at every vector of L. Asking for vanishing on the whole line, rather than at one representative, makes the set independent of any choice and meaningful for arbitrary polynomials: a nonzero constant equation cuts out the empty set and the zero equation cuts out everything. When each p i is homogeneous, testing one nonzero representative suffices, and in the standard affine chart where coordinate i is nonzero the zero locus is cut out by the dehomogenized equations dehomogenize i (p k) in the coordinate ratios.

The zero locus only depends on the ideal generated by the equations. In particular reindexing and adding or removing equations lying in that ideal do not change it. Replacing equations by positive powers changes the ideal but not its radical, and does not change the zero locus either: it is a reduced zero set, not a presentation. Unions of families of equations give intersections of zero loci, and pulling equations back along an injective linear map ℂ^N → ℂ^M computes the preimage under the induced map of projective spaces.

Main definitions

• TauCeti.complexProjectiveZeroLocus p: the common zero locus of the family p in Projectivization ℂ (Fin N → ℂ).

Main results

• TauCeti.complexProjectiveZeroLocus_mk_iff_forall_smul: the class of a nonzero vector v lies in the zero locus exactly when every p i vanishes on every multiple of v.
• TauCeti.complexProjectiveZeroLocus_mk_iff: for homogeneous equations, the class of a nonzero vector v lies in the zero locus exactly when every p i vanishes at v.
• TauCeti.complexProjectiveZeroLocus_mk_iff_dehomogenize and TauCeti.complexProjectiveZeroLocus_mk_insertNth_iff and TauCeti.mem_complexProjectiveZeroLocus_iff_eval_affineChart: the equations of the zero locus in the standard affine charts.
• TauCeti.complexProjectiveZeroLocus_subset_of_forall_mem_span: equations lying in the ideal generated by another family vanish on its zero locus.
• TauCeti.complexProjectiveZeroLocus_eq_of_span_eq: the zero locus only depends on the ideal generated by the equations.
• TauCeti.complexProjectiveZeroLocus_sumElim and TauCeti.complexProjectiveZeroLocus_sigma: unions of families of equations cut out intersections of zero loci.
• TauCeti.complexProjectiveZeroLocus_pow: replacing equations by positive powers does not change the zero locus.
• TauCeti.preimage_map_complexProjectiveZeroLocus: the preimage of a zero locus under the projective map induced by an injective linear map is the zero locus of the pulled-back equations.

def TauCeti.complexProjectiveZeroLocus {N : ℕ} {ι : Type u_1} (p : ι → MvPolynomial (Fin N) ℂ) : Set (Projectivization ℂ (Fin N → ℂ))

The common zero locus of a family of polynomials in N variables, as a set of complex lines in ℂ^N: a line belongs to it when every polynomial of the family vanishes at every vector of the line. The line of L is L.submodule, which is the underlying submodule of Projectivization.equivSubmodule ℂ (Fin N → ℂ) L.

@[simp]

theorem TauCeti.mem_complexProjectiveZeroLocus {N : ℕ} {ι : Type u_1} {p : ι → MvPolynomial (Fin N) ℂ} {L : Projectivization ℂ (Fin N → ℂ)} : L ∈ complexProjectiveZeroLocus p ↔ ∀ (i : ι), ∀ v ∈ L.submodule, (MvPolynomial.eval v) (p i) = 0

Membership in the zero locus unfolds to vanishing on every vector of the line.

theorem TauCeti.complexProjectiveZeroLocus_mk_iff_forall_smul {N : ℕ} {ι : Type u_1} {p : ι → MvPolynomial (Fin N) ℂ} (v : Fin N → ℂ) (hv : v ≠ 0) : Projectivization.mk ℂ v hv ∈ complexProjectiveZeroLocus p ↔ ∀ (i : ι) (c : ℂ), (MvPolynomial.eval (c • v)) (p i) = 0

The class of a nonzero vector v lies in the zero locus exactly when every equation vanishes at every scalar multiple of v. No homogeneity is needed.

theorem TauCeti.complexProjectiveZeroLocus_mk_iff {N : ℕ} {ι : Type u_1} {p : ι → MvPolynomial (Fin N) ℂ} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) (v : Fin N → ℂ) (hv : v ≠ 0) : Projectivization.mk ℂ v hv ∈ complexProjectiveZeroLocus p ↔ ∀ (i : ι), (MvPolynomial.eval v) (p i) = 0

For homogeneous equations, the class of a nonzero vector v lies in the zero locus exactly when every equation vanishes at v. This includes equations of degree zero, which are constants and vanish at v exactly when they are zero.

theorem TauCeti.mem_complexProjectiveZeroLocus_iff_eval_rep {N : ℕ} {ι : Type u_1} {p : ι → MvPolynomial (Fin N) ℂ} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) (L : Projectivization ℂ (Fin N → ℂ)) : L ∈ complexProjectiveZeroLocus p ↔ ∀ (i : ι), (MvPolynomial.eval L.rep) (p i) = 0

For homogeneous equations, membership in the zero locus can be tested on the chosen representative L.rep.

theorem TauCeti.complexProjectiveZeroLocus_mk_iff_dehomogenize {ι : Type u_1} {n : ℕ} {p : ι → MvPolynomial (Fin (n + 1)) ℂ} {d : ι → ℕ} (hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) (v : Fin (n + 1) → ℂ) {i : Fin (n + 1)} (hi : v i ≠ 0) : Projectivization.mk ℂ v ⋯ ∈ complexProjectiveZeroLocus p ↔ ∀ (k : ι), (MvPolynomial.eval fun (j : Fin n) => v (i.succAbove j) / v i) ((dehomogenize i) (p k)) = 0

Chart equations. In the standard affine chart where coordinate i is nonzero, a homogeneous family cuts out the zero locus of its dehomogenizations: the class of v with v i ≠ 0 lies in the zero locus exactly when every dehomogenize i (p k) vanishes at the coordinate ratios v (i.succAbove j) / v i.

theorem TauCeti.complexProjectiveZeroLocus_mk_insertNth_iff {ι : Type u_1} {n : ℕ} {p : ι → MvPolynomial (Fin (n + 1)) ℂ} {d : ι → ℕ} (hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) (i : Fin (n + 1)) (z : Fin n → ℂ) : Projectivization.mk ℂ (i.insertNth 1 z) ⋯ ∈ complexProjectiveZeroLocus p ↔ ∀ (k : ι), (MvPolynomial.eval z) ((dehomogenize i) (p k)) = 0

The inverse chart: the class of the vector [z₀ : ⋯ : 1 : ⋯ : zₙ₋₁], with 1 inserted at coordinate i, lies in the zero locus of a homogeneous family exactly when z is a common zero of the dehomogenizations dehomogenize i (p k).

theorem TauCeti.mem_complexProjectiveZeroLocus_iff_eval_affineChart {ι : Type u_1} {n : ℕ} {p : ι → MvPolynomial (Fin (n + 1)) ℂ} {d : ι → ℕ} (hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) {i : Fin (n + 1)} {L : Projectivization ℂ (Fin (n + 1) → ℂ)} (hL : L ∈ Projectivization.affineOpen i) : L ∈ complexProjectiveZeroLocus p ↔ ∀ (k : ι), (MvPolynomial.eval (↑(Projectivization.affineChart i) L)) ((dehomogenize i) (p k)) = 0

Chart equations on the affine open. A point of the standard affine open where coordinate i is nonzero lies in the zero locus of a homogeneous family exactly when its chart coordinates Projectivization.affineChart i L are a common zero of the dehomogenizations dehomogenize i (p k).

@[simp]

theorem TauCeti.complexProjectiveZeroLocus_of_fin_zero {ι : Type u_1} (p : ι → MvPolynomial (Fin 0) ℂ) : complexProjectiveZeroLocus p = ∅

In ℂ⁰ there are no lines, so every zero locus is empty.

@[simp]

theorem TauCeti.complexProjectiveZeroLocus_of_isEmpty {N : ℕ} {ι : Type u_1} [IsEmpty ι] (p : ι → MvPolynomial (Fin N) ℂ) : complexProjectiveZeroLocus p = Set.univ

The empty family of equations cuts out the whole projective space.

@[simp]

theorem TauCeti.complexProjectiveZeroLocus_zero {N : ℕ} {ι : Type u_1} : complexProjectiveZeroLocus 0 = Set.univ

The family of zero equations cuts out the whole projective space.

theorem TauCeti.complexProjectiveZeroLocus_eq_empty_of_eq_C {N : ℕ} {ι : Type u_1} {p : ι → MvPolynomial (Fin N) ℂ} {i : ι} {c : ℂ} (hpi : p i = MvPolynomial.C c) (hc : c ≠ 0) : complexProjectiveZeroLocus p = ∅

A nonzero constant equation cuts out the empty set.

theorem TauCeti.complexProjectiveZeroLocus_subset_of_forall_mem_span {N : ℕ} {ι : Type u_1} {κ : Type u_2} {p : ι → MvPolynomial (Fin N) ℂ} {q : κ → MvPolynomial (Fin N) ℂ} (h : ∀ (j : κ), q j ∈ Ideal.span (Set.range p)) : complexProjectiveZeroLocus p ⊆ complexProjectiveZeroLocus q

Every polynomial in the ideal generated by a family of equations vanishes on its zero locus: the zero locus of p is contained in that of q when each q j lies in that ideal.

theorem TauCeti.complexProjectiveZeroLocus_eq_of_span_eq {N : ℕ} {ι : Type u_1} {κ : Type u_2} {p : ι → MvPolynomial (Fin N) ℂ} {q : κ → MvPolynomial (Fin N) ℂ} (h : Ideal.span (Set.range p) = Ideal.span (Set.range q)) : complexProjectiveZeroLocus p = complexProjectiveZeroLocus q

The zero locus only depends on the ideal generated by the equations.

theorem TauCeti.complexProjectiveZeroLocus_subset_comp {N : ℕ} {ι : Type u_1} {κ : Type u_2} (p : ι → MvPolynomial (Fin N) ℂ) (e : κ → ι) : complexProjectiveZeroLocus p ⊆ complexProjectiveZeroLocus (p ∘ e)

Dropping equations enlarges the zero locus: a subfamily, indexed along any map e, has a larger zero locus.

theorem TauCeti.complexProjectiveZeroLocus_comp_of_surjective {N : ℕ} {ι : Type u_1} {κ : Type u_2} (p : ι → MvPolynomial (Fin N) ℂ) {e : κ → ι} (he : Function.Surjective e) : complexProjectiveZeroLocus (p ∘ e) = complexProjectiveZeroLocus p

Reindexing a family of equations along a surjection does not change its zero locus.

theorem TauCeti.complexProjectiveZeroLocus_sumElim {N : ℕ} {ι : Type u_1} {κ : Type u_2} (p : ι → MvPolynomial (Fin N) ℂ) (q : κ → MvPolynomial (Fin N) ℂ) : complexProjectiveZeroLocus (Sum.elim p q) = complexProjectiveZeroLocus p ∩ complexProjectiveZeroLocus q

Joining two families of equations intersects their zero loci.

theorem TauCeti.complexProjectiveZeroLocus_sumElim_of_forall_mem_span {N : ℕ} {ι : Type u_1} {κ : Type u_2} (p : ι → MvPolynomial (Fin N) ℂ) {q : κ → MvPolynomial (Fin N) ℂ} (h : ∀ (j : κ), q j ∈ Ideal.span (Set.range p)) : complexProjectiveZeroLocus (Sum.elim p q) = complexProjectiveZeroLocus p

Adding equations that lie in the ideal generated by a family does not change its zero locus.

theorem TauCeti.complexProjectiveZeroLocus_sigma {N : ℕ} {κ : Type u_2} {ι : κ → Type u_3} (p : (k : κ) → ι k → MvPolynomial (Fin N) ℂ) : (complexProjectiveZeroLocus fun (x : (k : κ) × ι k) => p x.fst x.snd) = ⋂ (k : κ), complexProjectiveZeroLocus (p k)

The union of a family of families of equations cuts out the intersection of their zero loci.

theorem TauCeti.complexProjectiveZeroLocus_pow {N : ℕ} {ι : Type u_1} (p : ι → MvPolynomial (Fin N) ℂ) {k : ι → ℕ} (hk : ∀ (i : ι), k i ≠ 0) : (complexProjectiveZeroLocus fun (i : ι) => p i ^ k i) = complexProjectiveZeroLocus p

Replacing each equation by a positive power does not change the zero locus.

theorem TauCeti.preimage_map_complexProjectiveZeroLocus {N : ℕ} {ι : Type u_1} {M : ℕ} (f : (Fin N → ℂ) →ₗ[ℂ] Fin M → ℂ) (hf : Function.Injective ⇑f) (q : ι → MvPolynomial (Fin M) ℂ) : Projectivization.map f hf ⁻¹' complexProjectiveZeroLocus q = complexProjectiveZeroLocus fun (i : ι) => (MvPolynomial.aeval (LinearMap.toMatrix' f).toMvPolynomial) (q i)

The preimage of a zero locus under the map of projective spaces induced by an injective linear map f : ℂ^N → ℂ^M is the zero locus of the equations pulled back along f, that is with each variable X j replaced by the j-th coordinate of f as a linear form.