zilber_pink_conjecture
Provedalgebraalgebraic-geometry
Zilber-Pink conjecture: Torsion anomalous subvarieties of an algebraic variety in a torus are contained in finitely many proper special subvarieties. Generalizes Manin-Mumford. Open in general.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem zilber_pink_conjecture (n : ℕ) (hn : 2 ≤ n)
(V : Set (Fin n → ℂ))
(hV_alg : ∃ (polys : List (MvPolynomial (Fin n) ℂ)),
V = {x | ∀ p ∈ polys, MvPolynomial.eval x p = 0}) :
∃ (finite_special : Finset (Set (Fin n → ℂ))),
{x ∈ V | ∃ (A : Matrix (Fin n) (Fin n) ℤ) (_ : A.det ≠ 0)
(_ : A.det ≠ 1 ∧ A.det ≠ -1),
∀ i : Fin n, ∑ j, (A i j : ℂ) * x j = 0} ⊆
⋃ S ∈ finite_special, S := by
sorrySource