Common zeros on products of projective planes

Scratch development, independent of Submission/Spec.lean. The multihomogeneity convention is coefficientwise, so the zero polynomial is homogeneous of every multidegree. No projective intersection theorem is assumed as an axiom.

@[reducible, inline]

abbrev KoetheMultiProjective.Vars (N : ℕ) : Type

The polynomial variables, grouped into triples.

Equations

• KoetheMultiProjective.Vars N = (Fin N × Fin 3)

def KoetheMultiProjective.blockDegree {N : ℕ} (d : Vars N →₀ ℕ) (b : Fin N) : ℕ

The degree of an exponent vector in one block.

Equations

• KoetheMultiProjective.blockDegree d b = ∑ j : Fin 3, d (b, j)

@[simp]

theorem KoetheMultiProjective.blockDegree_zero {N : ℕ} (b : Fin N) : blockDegree 0 b = 0

@[simp]

theorem KoetheMultiProjective.blockDegree_add {N : ℕ} (d e : Vars N →₀ ℕ) (b : Fin N) : blockDegree (d + e) b = blockDegree d b + blockDegree e b

def KoetheMultiProjective.Balanced {N : ℕ} (d : Vars N →₀ ℕ) : Prop

All block degrees of an exponent vector are equal.

Equations

• KoetheMultiProjective.Balanced d = ∀ (b c : Fin N), KoetheMultiProjective.blockDegree d b = KoetheMultiProjective.blockDegree d c

@[instance_reducible]

instance KoetheMultiProjective.instDecidableBalanced {N : ℕ} (d : Vars N →₀ ℕ) : Decidable (Balanced d)

Equations

• KoetheMultiProjective.instDecidableBalanced d = KoetheMultiProjective.instDecidableBalanced._aux_1 d

@[simp]

theorem KoetheMultiProjective.balanced_zero {N : ℕ} : Balanced 0

theorem KoetheMultiProjective.Balanced.add {N : ℕ} {d e : Vars N →₀ ℕ} (hd : Balanced d) (he : Balanced e) : Balanced (d + e)

theorem KoetheMultiProjective.Balanced.add_iff_right {N : ℕ} {d e : Vars N →₀ ℕ} (hd : Balanced d) : Balanced (d + e) ↔ Balanced e

def KoetheMultiProjective.IsMultiHomogeneous {k : Type u_1} {N : ℕ} [CommSemiring k] (f : MvPolynomial (Vars N) k) (r : Fin N → ℕ) : Prop

Coefficientwise multihomogeneity with a specified degree in each block.

Equations

• KoetheMultiProjective.IsMultiHomogeneous f r = ∀ (d : KoetheMultiProjective.Vars N →₀ ℕ), MvPolynomial.coeff d f ≠ 0 → ∀ (b : Fin N), KoetheMultiProjective.blockDegree d b = r b

def KoetheMultiProjective.IsMultiHomogeneousOfDegree {k : Type u_1} {N : ℕ} [CommSemiring k] (f : MvPolynomial (Vars N) k) (r : ℕ) : Prop

Every nonzero monomial has the same degree r in every block.

Equations

• KoetheMultiProjective.IsMultiHomogeneousOfDegree f r = KoetheMultiProjective.IsMultiHomogeneous f fun (x : Fin N) => r

def KoetheMultiProjective.HasBalancedSupport {k : Type u_1} {N : ℕ} [CommSemiring k] (f : MvPolynomial (Vars N) k) : Prop

Polynomials all of whose monomials have balanced block degrees. Different monomials may have different common degrees.

Equations

• KoetheMultiProjective.HasBalancedSupport f = ∀ (d : KoetheMultiProjective.Vars N →₀ ℕ), MvPolynomial.coeff d f ≠ 0 → KoetheMultiProjective.Balanced d

theorem KoetheMultiProjective.IsMultiHomogeneousOfDegree.hasBalancedSupport {k : Type u_1} {N : ℕ} [CommSemiring k] {f : MvPolynomial (Vars N) k} {r : ℕ} (hf : IsMultiHomogeneousOfDegree f r) : HasBalancedSupport f

@[simp]

theorem KoetheMultiProjective.isMultiHomogeneous_zero {k : Type u_1} {N : ℕ} [CommSemiring k] (r : Fin N → ℕ) : IsMultiHomogeneous 0 r

@[simp]

theorem KoetheMultiProjective.isMultiHomogeneousOfDegree_zero {k : Type u_1} {N : ℕ} [CommSemiring k] (r : ℕ) : IsMultiHomogeneousOfDegree 0 r

theorem KoetheMultiProjective.isMultiHomogeneous_monomial {k : Type u_1} {N : ℕ} [CommSemiring k] {d : Vars N →₀ ℕ} {r : Fin N → ℕ} (hd : ∀ (b : Fin N), blockDegree d b = r b) (a : k) : IsMultiHomogeneous ((MvPolynomial.monomial d) a) r

theorem KoetheMultiProjective.IsMultiHomogeneous.add {k : Type u_1} {N : ℕ} [CommSemiring k] {p q : MvPolynomial (Vars N) k} {r : Fin N → ℕ} (hp : IsMultiHomogeneous p r) (hq : IsMultiHomogeneous q r) : IsMultiHomogeneous (p + q) r

theorem KoetheMultiProjective.IsMultiHomogeneous.smul {k : Type u_1} {N : ℕ} [CommSemiring k] {p : MvPolynomial (Vars N) k} {r : Fin N → ℕ} (hp : IsMultiHomogeneous p r) (a : k) : IsMultiHomogeneous (a • p) r

theorem KoetheMultiProjective.IsMultiHomogeneous.mul {k : Type u_1} {N : ℕ} [CommSemiring k] {p q : MvPolynomial (Vars N) k} {r s : Fin N → ℕ} (hp : IsMultiHomogeneous p r) (hq : IsMultiHomogeneous q s) : IsMultiHomogeneous (p * q) (r + s)

theorem KoetheMultiProjective.IsMultiHomogeneous.pow {k : Type u_1} {N : ℕ} [CommSemiring k] {p : MvPolynomial (Vars N) k} {r : Fin N → ℕ} (hp : IsMultiHomogeneous p r) (n : ℕ) : IsMultiHomogeneous (p ^ n) fun (b : Fin N) => n * r b

theorem KoetheMultiProjective.IsMultiHomogeneousOfDegree.add {k : Type u_1} {N : ℕ} [CommSemiring k] {p q : MvPolynomial (Vars N) k} {r : ℕ} (hp : IsMultiHomogeneousOfDegree p r) (hq : IsMultiHomogeneousOfDegree q r) : IsMultiHomogeneousOfDegree (p + q) r

theorem KoetheMultiProjective.IsMultiHomogeneousOfDegree.mul {k : Type u_1} {N : ℕ} [CommSemiring k] {p q : MvPolynomial (Vars N) k} {r s : ℕ} (hp : IsMultiHomogeneousOfDegree p r) (hq : IsMultiHomogeneousOfDegree q s) : IsMultiHomogeneousOfDegree (p * q) (r + s)

theorem KoetheMultiProjective.IsMultiHomogeneousOfDegree.pow {k : Type u_1} {N : ℕ} [CommSemiring k] {p : MvPolynomial (Vars N) k} {r : ℕ} (hp : IsMultiHomogeneousOfDegree p r) (n : ℕ) : IsMultiHomogeneousOfDegree (p ^ n) (n * r)

theorem KoetheMultiProjective.hasBalancedSupport_monomial {k : Type u_1} {N : ℕ} [CommSemiring k] {d : Vars N →₀ ℕ} (hd : Balanced d) (a : k) : HasBalancedSupport ((MvPolynomial.monomial d) a)

theorem KoetheMultiProjective.hasBalancedSupport_add {k : Type u_1} {N : ℕ} [CommSemiring k] {p q : MvPolynomial (Vars N) k} (hp : HasBalancedSupport p) (hq : HasBalancedSupport q) : HasBalancedSupport (p + q)

theorem KoetheMultiProjective.hasBalancedSupport_mul {k : Type u_1} {N : ℕ} [CommSemiring k] {p q : MvPolynomial (Vars N) k} (hp : HasBalancedSupport p) (hq : HasBalancedSupport q) : HasBalancedSupport (p * q)

def KoetheMultiProjective.balancedAlgebra (k : Type u_2) [CommSemiring k] (N : ℕ) : Subalgebra k (MvPolynomial (Vars N) k)

The diagonal (balanced-degree) monomial subalgebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem KoetheMultiProjective.mem_balancedAlgebra {k : Type u_1} {N : ℕ} [CommSemiring k] {p : MvPolynomial (Vars N) k} : p ∈ balancedAlgebra k N ↔ HasBalancedSupport p

noncomputable def KoetheMultiProjective.segreExponent {N : ℕ} (j : Fin N → Fin 3) : Vars N →₀ ℕ

Exponent vector of a degree-one Segre coordinate.

Equations

• KoetheMultiProjective.segreExponent j = ∑ b : Fin N, Finsupp.single (b, j b) 1

@[simp]

theorem KoetheMultiProjective.segreExponent_apply {N : ℕ} (j : Fin N → Fin 3) (b : Fin N) (c : Fin 3) : (segreExponent j) (b, c) = if j b = c then 1 else 0

@[simp]

theorem KoetheMultiProjective.blockDegree_segreExponent {N : ℕ} (j : Fin N → Fin 3) (b : Fin N) : blockDegree (segreExponent j) b = 1

theorem KoetheMultiProjective.balanced_segreExponent {N : ℕ} (j : Fin N → Fin 3) : Balanced (segreExponent j)

noncomputable def KoetheMultiProjective.segreMonomial {k : Type u_1} {N : ℕ} [CommSemiring k] (j : Fin N → Fin 3) : MvPolynomial (Vars N) k

A degree-one Segre coordinate, as a polynomial in the original triples.

Equations

• KoetheMultiProjective.segreMonomial j = ∏ b : Fin N, MvPolynomial.X (b, j b)

theorem KoetheMultiProjective.segreMonomial_eq_monomial {k : Type u_1} {N : ℕ} [CommSemiring k] (j : Fin N → Fin 3) : segreMonomial j = (MvPolynomial.monomial (segreExponent j)) 1

theorem KoetheMultiProjective.isMultiHomogeneousOfDegree_segreMonomial {k : Type u_1} {N : ℕ} [CommSemiring k] (j : Fin N → Fin 3) : IsMultiHomogeneousOfDegree (segreMonomial j) 1

theorem KoetheMultiProjective.segreMonomial_mem {k : Type u_1} {N : ℕ} [CommSemiring k] (j : Fin N → Fin 3) : segreMonomial j ∈ balancedAlgebra k N

theorem KoetheMultiProjective.exponent_eq_zero_of_blockDegree_zero {N : ℕ} {d : Vars N →₀ ℕ} (hd : ∀ (b : Fin N), blockDegree d b = 0) : d = 0

theorem KoetheMultiProjective.exists_segreExponent_le {N : ℕ} {d : Vars N →₀ ℕ} {r : ℕ} (hd : ∀ (b : Fin N), blockDegree d b = r + 1) : ∃ (j : Fin N → Fin 3), segreExponent j ≤ d

theorem KoetheMultiProjective.monomial_mem_adjoin_segre {k : Type u_1} {N : ℕ} [CommSemiring k] {d : Vars N →₀ ℕ} {r : ℕ} (hd : ∀ (b : Fin N), blockDegree d b = r) (a : k) : (MvPolynomial.monomial d) a ∈ Algebra.adjoin k (Set.range segreMonomial)

A balanced monomial factors into degree-one Segre monomials. This is the finite-generation step, proved by induction on the common degree.

theorem KoetheMultiProjective.adjoin_segre_eq_balancedAlgebra {k : Type u_1} {N : ℕ} [CommSemiring k] [NeZero N] : Algebra.adjoin k (Set.range segreMonomial) = balancedAlgebra k N

The balanced subalgebra is generated by the finitely many Segre coordinates.

instance KoetheMultiProjective.balancedAlgebra_isNoetherianRing {k : Type u_1} {N : ℕ} [CommRing k] [IsNoetherianRing k] [NeZero N] : IsNoetherianRing ↥(balancedAlgebra k N)

noncomputable def KoetheMultiProjective.balancedPart {k : Type u_1} {N : ℕ} [CommSemiring k] : MvPolynomial (Vars N) k →ₗ[k] MvPolynomial (Vars N) k

Keep just the monomials whose block degrees are all equal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem KoetheMultiProjective.coeff_balancedPart {k : Type u_1} {N : ℕ} [CommSemiring k] (p : MvPolynomial (Vars N) k) (d : Vars N →₀ ℕ) : MvPolynomial.coeff d (balancedPart p) = if Balanced d then MvPolynomial.coeff d p else 0

theorem KoetheMultiProjective.balancedPart_mem {k : Type u_1} {N : ℕ} [CommSemiring k] (p : MvPolynomial (Vars N) k) : balancedPart p ∈ balancedAlgebra k N

@[simp]

theorem KoetheMultiProjective.balancedPart_of_mem {k : Type u_1} {N : ℕ} [CommSemiring k] {p : MvPolynomial (Vars N) k} (hp : p ∈ balancedAlgebra k N) : balancedPart p = p

@[simp]

theorem KoetheMultiProjective.balancedPart_monomial {k : Type u_1} {N : ℕ} [CommSemiring k] (d : Vars N →₀ ℕ) (a : k) : balancedPart ((MvPolynomial.monomial d) a) = if Balanced d then (MvPolynomial.monomial d) a else 0

theorem KoetheMultiProjective.balancedPart_monomial_mul {k : Type u_1} {N : ℕ} [CommSemiring k] {d : Vars N →₀ ℕ} (hd : Balanced d) (a : k) (q : MvPolynomial (Vars N) k) : balancedPart ((MvPolynomial.monomial d) a * q) = (MvPolynomial.monomial d) a * balancedPart q

theorem KoetheMultiProjective.balancedPart_mul {k : Type u_1} {N : ℕ} [CommSemiring k] {p : MvPolynomial (Vars N) k} (hp : p ∈ balancedAlgebra k N) (q : MvPolynomial (Vars N) k) : balancedPart (p * q) = p * balancedPart q

The balanced-monomial projection is linear over the whole balanced subalgebra, not merely over the coefficient field.

noncomputable def KoetheMultiProjective.balancedRetract {k : Type u_1} {N : ℕ} [CommSemiring k] : MvPolynomial (Vars N) k →ₗ[k] ↥(balancedAlgebra k N)

The same projection with codomain restricted to the balanced algebra.

Equations

• KoetheMultiProjective.balancedRetract = LinearMap.codRestrict (Subalgebra.toSubmodule (KoetheMultiProjective.balancedAlgebra k N)) KoetheMultiProjective.balancedPart ⋯

@[simp]

theorem KoetheMultiProjective.coe_balancedRetract {k : Type u_1} {N : ℕ} [CommSemiring k] (p : MvPolynomial (Vars N) k) : ↑(balancedRetract p) = balancedPart p

@[simp]

theorem KoetheMultiProjective.balancedRetract_coe {k : Type u_1} {N : ℕ} [CommSemiring k] (p : ↥(balancedAlgebra k N)) : balancedRetract ↑p = p

@[simp]

theorem KoetheMultiProjective.balancedRetract_mul {k : Type u_1} {N : ℕ} [CommSemiring k] (p : ↥(balancedAlgebra k N)) (q : MvPolynomial (Vars N) k) : balancedRetract (↑p * q) = p * balancedRetract q

theorem KoetheMultiProjective.mem_span_range_coe_iff {k : Type u_1} {N : ℕ} [CommSemiring k] {ι : Type u_2} [Finite ι] (f : ι → ↥(balancedAlgebra k N)) (p : ↥(balancedAlgebra k N)) : ↑p ∈ Ideal.span (Set.range fun (i : ι) => ↑(f i)) ↔ p ∈ Ideal.span (Set.range f)

Extending an ideal generated by balanced polynomials to the ambient polynomial ring and contracting it back introduces no new balanced elements.

theorem KoetheMultiProjective.mem_radical_span_range_coe_iff {k : Type u_1} {N : ℕ} [CommSemiring k] {ι : Type u_2} [Finite ι] (f : ι → ↥(balancedAlgebra k N)) (p : ↥(balancedAlgebra k N)) : ↑p ∈ (Ideal.span (Set.range fun (i : ι) => ↑(f i))).radical ↔ p ∈ (Ideal.span (Set.range f)).radical

noncomputable def KoetheMultiProjective.segre {k : Type u_1} {N : ℕ} [Field k] (j : Fin N → Fin 3) : ↥(balancedAlgebra k N)

A Segre coordinate as an element of the balanced subalgebra.

Equations

• KoetheMultiProjective.segre j = ⟨KoetheMultiProjective.segreMonomial j, ⋯⟩

@[simp]

theorem KoetheMultiProjective.coe_segre {k : Type u_1} {N : ℕ} [Field k] (j : Fin N → Fin 3) : ↑(segre j) = segreMonomial j

theorem KoetheMultiProjective.segreMonomial_ne_zero {k : Type u_1} {N : ℕ} [Field k] (j : Fin N → Fin 3) : segreMonomial j ≠ 0

@[simp]

theorem KoetheMultiProjective.constantCoeff_segreMonomial {k : Type u_1} {N : ℕ} [Field k] [NeZero N] (j : Fin N → Fin 3) : MvPolynomial.constantCoeff (segreMonomial j) = 0

noncomputable def KoetheMultiProjective.killVars {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) : MvPolynomial (Vars N) k →ₐ[k] MvPolynomial (Vars N) k

Set a specified finite set of ambient variables to zero.

Equations

• KoetheMultiProjective.killVars s = MvPolynomial.aeval fun (v : KoetheMultiProjective.Vars N) => if v ∈ s then 0 else MvPolynomial.X v

@[simp]

theorem KoetheMultiProjective.killVars_X {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) (v : Vars N) : (killVars s) (MvPolynomial.X v) = if v ∈ s then 0 else MvPolynomial.X v

theorem KoetheMultiProjective.killVars_comp_of_subset {k : Type u_1} {N : ℕ} [Field k] {s t : Finset (Vars N)} (hst : s ⊆ t) : (killVars t).comp (killVars s) = killVars t

theorem KoetheMultiProjective.zero_aeval_comp_killVars {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) : (MvPolynomial.aeval fun (x : Vars N) => 0).comp (killVars s) = MvPolynomial.aeval fun (x : Vars N) => 0

noncomputable def KoetheMultiProjective.killedIdeal {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) : Ideal ↥(balancedAlgebra k N)

Contract a prime variable ideal to the balanced subalgebra.

Equations

• KoetheMultiProjective.killedIdeal s = RingHom.ker ((KoetheMultiProjective.killVars s).comp (KoetheMultiProjective.balancedAlgebra k N).val).toRingHom

@[simp]

theorem KoetheMultiProjective.mem_killedIdeal {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) (p : ↥(balancedAlgebra k N)) : p ∈ killedIdeal s ↔ (killVars s) ↑p = 0

instance KoetheMultiProjective.killedIdeal_isPrime {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) : (killedIdeal s).IsPrime

noncomputable def KoetheMultiProjective.vertexIdeal (k : Type u_2) [Field k] (N : ℕ) : Ideal ↥(balancedAlgebra k N)

The vertex of the affine Segre cone: the augmentation ideal.

Equations

• KoetheMultiProjective.vertexIdeal k N = RingHom.ker ((MvPolynomial.aeval fun (x : KoetheMultiProjective.Vars N) => 0).comp (KoetheMultiProjective.balancedAlgebra k N).val).toRingHom

@[simp]

theorem KoetheMultiProjective.mem_vertexIdeal {k : Type u_1} {N : ℕ} [Field k] (p : ↥(balancedAlgebra k N)) : p ∈ vertexIdeal k N ↔ MvPolynomial.constantCoeff ↑p = 0

instance KoetheMultiProjective.vertexIdeal_isPrime {k : Type u_1} {N : ℕ} [Field k] : (vertexIdeal k N).IsPrime

theorem KoetheMultiProjective.killedIdeal_mono {k : Type u_1} {N : ℕ} [Field k] {s t : Finset (Vars N)} (hst : s ⊆ t) : killedIdeal s ≤ killedIdeal t

theorem KoetheMultiProjective.killedIdeal_le_vertexIdeal {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) : killedIdeal s ≤ vertexIdeal k N

theorem KoetheMultiProjective.killVars_segreMonomial_of_disjoint {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) (j : Fin N → Fin 3) (hj : ∀ (b : Fin N), (b, j b) ∉ s) : (killVars s) (segreMonomial j) = segreMonomial j

theorem KoetheMultiProjective.killVars_segreMonomial_of_mem {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) (j : Fin N → Fin 3) (b : Fin N) (hb : (b, j b) ∈ s) : (killVars s) (segreMonomial j) = 0

def KoetheMultiProjective.separatingChoice {N : ℕ} (v : Vars N) (b : Fin N) : Fin 3

Choose the newly killed variable in its block and the protected coordinate 2 in every other block.

Equations

• KoetheMultiProjective.separatingChoice v b = if b = v.1 then v.2 else 2

theorem KoetheMultiProjective.separatingChoice_avoids {N : ℕ} {s : Finset (Vars N)} (hprotect : ∀ (b : Fin N), (b, 2) ∉ s) {v : Vars N} (hv : v ∉ s) (b : Fin N) : (b, separatingChoice v b) ∉ s

theorem KoetheMultiProjective.killedIdeal_lt_insert {k : Type u_1} {N : ℕ} [Field k] {s : Finset (Vars N)} (hprotect : ∀ (b : Fin N), (b, 2) ∉ s) {v : Vars N} (hv : v ∉ s) : killedIdeal s < killedIdeal (insert v s)

Each additional killed coordinate strictly increases the contracted prime ideal.

theorem KoetheMultiProjective.killedIdeal_lt_vertexIdeal {k : Type u_1} {N : ℕ} [Field k] [NeZero N] {s : Finset (Vars N)} (hprotect : ∀ (b : Fin N), (b, 2) ∉ s) : killedIdeal s < vertexIdeal k N

The final strict step kills the remaining positive-degree balanced monomials.

theorem KoetheMultiProjective.card_le_height_killedIdeal {k : Type u_1} {N : ℕ} [Field k] (s : Finset (Vars N)) (hprotect : ∀ (b : Fin N), (b, 2) ∉ s) : ↑s.card ≤ (killedIdeal s).height

The height of a contracted variable ideal is at least the number of killed coordinates, as long as one coordinate in every block remains protected.

theorem KoetheMultiProjective.vertexIdeal_height_lower_bound {k : Type u_1} {N : ℕ} [Field k] [NeZero N] : 2 * ↑N + 1 ≤ (vertexIdeal k N).height

The Segre cone vertex has height at least 2*N + 1. The proof constructs all 2*N + 1 strict prime-ideal steps explicitly.

theorem KoetheMultiProjective.IsMultiHomogeneousOfDegree.constantCoeff_eq_zero {k : Type u_1} {N : ℕ} [Field k] [NeZero N] {f : MvPolynomial (Vars N) k} {r : ℕ} (hf : IsMultiHomogeneousOfDegree f r) (hr : 0 < r) : MvPolynomial.constantCoeff f = 0

theorem KoetheMultiProjective.eval_eq_constantCoeff_of_block_zero {k : Type u_1} {N : ℕ} [Field k] [NeZero N] {p : MvPolynomial (Vars N) k} (hp : p ∈ balancedAlgebra k N) {x : Vars N → k} {b : Fin N} (hx : ∀ (j : Fin 3), x (b, j) = 0) : (MvPolynomial.eval x) p = MvPolynomial.constantCoeff p

On an assignment with one zero block, any balanced polynomial evaluates to its constant coefficient.

theorem KoetheMultiProjective.radical_span_eq_vertex_of_no_common_zero {k : Type u_1} {N : ℕ} [Field k] [IsAlgClosed k] [NeZero N] {ι : Type u_2} [Finite ι] (f : ι → ↥(balancedAlgebra k N)) (hf : ∀ (i : ι), f i ∈ vertexIdeal k N) (hno : ¬∃ (x : Vars N → k), (∀ (b : Fin N), ∃ (j : Fin 3), x (b, j) ≠ 0) ∧ ∀ (i : ι), (MvPolynomial.eval x) ↑(f i) = 0) : (Ideal.span (Set.range f)).radical = vertexIdeal k N

If balanced polynomials with zero constant term have no common zero with all blocks nonzero, their ideal in the balanced subalgebra has radical the vertex. This is the affine Nullstellensatz plus the explicitly proved retraction.

theorem KoetheMultiProjective.exists_common_zero_balanced {k : Type u_1} {N : ℕ} [Field k] [IsAlgClosed k] [NeZero N] {q : ℕ} (hq : q ≤ 2 * N) (f : Fin q → ↥(balancedAlgebra k N)) (hf : ∀ (i : Fin q), f i ∈ vertexIdeal k N) : ∃ (x : Vars N → k), (∀ (b : Fin N), ∃ (j : Fin 3), x (b, j) ≠ 0) ∧ ∀ (i : Fin q), (MvPolynomial.eval x) ↑(f i) = 0

A slightly stronger algebraic theorem: the polynomials may be sums of balanced monomials of different degrees, provided all constant coefficients vanish.

theorem KoetheMultiProjective.exists_common_zero {k : Type u_1} {N : ℕ} [Field k] [IsAlgClosed k] {q r : ℕ} (f : Fin q → MvPolynomial (Fin N × Fin 3) k) (hN : 0 < N) (hr : 0 < r) (hq : q ≤ 2 * N) (hf : ∀ (i : Fin q), IsMultiHomogeneousOfDegree (f i) r) : ∃ (x : Fin N × Fin 3 → k), (∀ (b : Fin N), (fun (j : Fin 3) => x (b, j)) ≠ 0) ∧ ∀ (i : Fin q), (MvPolynomial.eval x) (f i) = 0

Multiprojective common-zero theorem. Over an algebraically closed field, at most 2*N polynomials of common positive degree in every one of N blocks of three variables have a common zero with no zero block.

The proof is entirely affine commutative algebra: finite generation of the balanced monomial algebra, a linear retraction, the Nullstellensatz, an explicit chain of prime ideals, and Krull's height theorem.

theorem KoetheMultiProjective.exists_common_zero_of_coeff {k : Type u_1} {N : ℕ} [Field k] [IsAlgClosed k] {q r : ℕ} (f : Fin q → MvPolynomial (Fin N × Fin 3) k) (hN : 0 < N) (hr : 0 < r) (hq : q ≤ 2 * N) (hf : ∀ (i : Fin q) (d : Fin N × Fin 3 →₀ ℕ), MvPolynomial.coeff d (f i) ≠ 0 → ∀ (b : Fin N), ∑ j : Fin 3, d (b, j) = r) : ∃ (x : Fin N × Fin 3 → k), (∀ (b : Fin N), (fun (j : Fin 3) => x (b, j)) ≠ 0) ∧ ∀ (i : Fin q), (MvPolynomial.eval x) (f i) = 0

An entry point with the multihomogeneity hypothesis fully expanded in terms of coefficients and blockwise sums of exponents.

theorem KoetheMultiProjective.exists_common_zero_vectors {k : Type u_1} {N : ℕ} [Field k] [IsAlgClosed k] {q r : ℕ} (f : Fin q → MvPolynomial (Fin N × Fin 3) k) (hN : 0 < N) (hr : 0 < r) (hq : q ≤ 2 * N) (hf : ∀ (i : Fin q), IsMultiHomogeneousOfDegree (f i) r) : ∃ (x : Fin N → Fin 3 → k), (∀ (b : Fin N), x b ≠ 0) ∧ ∀ (i : Fin q), (MvPolynomial.eval fun (v : Fin N × Fin 3) => x v.1 v.2) (f i) = 0

The same result with the assignment written as a family of nonzero vectors.