Lemma 8.8, geometric part: finitely many orbits cannot cover a large zero set

local-ray-geometry.tex (lem:dimension-infinity): "The representation variety is a nonempty zero set of at most F scalar polynomial equations in affine N-space; the zero arrow assignment is a point. Every component of such a zero set has dimension at least N − F. The change-of-basis group has dimension D, and its simultaneous scalar subgroup stabilizes every representation. An orbit has dimension equal to that of the group minus that of the stabilizer, so each orbit has dimension at most D − 1. The variety cannot be a finite union of these orbits."

Setting: arrows a : s a → t a between vertices with dimensions d, representation space of matrices x_a ∈ k^{d(t a) × d(s a)}, the group ∏ GL_{d v} acting by x_a ↦ g_{t a} x_a g_{s a}⁻¹. Formalization of the dimension count:

• (step 1) the zero set X of F polynomials vanishing at 0: dim k[x]/I ≥ N − F by Krull's height theorem at the origin, whose height is N (a chain of coordinate primes);
• (step 2) an orbit is covered by the images of the charts g_c = 1 of the group (scalar invariance), each a localization of a polynomial ring in D − 1 variables; the vanishing ideal J_{x,c} of a chart image is prime and dim k[x]/J_{x,c} ≤ D − 1 (Noether normalization and transcendence degree);
• (step 3) by the Nullstellensatz a prime over I contains some J_{x,c}, so dim k[x]/I ≤ D − 1.

Step 1: the height of the origin and Krull's height theorem

noncomputable def MultiplicativeBasisDeformations.OrbitDim.killBelow {k : Type u_1} [Field k] {σ : Type} [Fintype σ] (e : σ ≃ Fin (Fintype.card σ)) (j : ℕ) : MvPolynomial σ k →ₐ[k] MvPolynomial σ k

Kill the variables of index below j.

noncomputable def MultiplicativeBasisDeformations.OrbitDim.Pj {k : Type u_1} [Field k] {σ : Type} [Fintype σ] (e : σ ≃ Fin (Fintype.card σ)) (j : ℕ) : Ideal (MvPolynomial σ k)

The coordinate primes.

theorem MultiplicativeBasisDeformations.OrbitDim.Pj_isPrime {k : Type u_1} [Field k] {σ : Type} [Fintype σ] [DecidableEq σ] (e : σ ≃ Fin (Fintype.card σ)) (j : ℕ) : (Pj e j).IsPrime

theorem MultiplicativeBasisDeformations.OrbitDim.killBelow_comp {k : Type u_1} [Field k] {σ : Type} [Fintype σ] [DecidableEq σ] (e : σ ≃ Fin (Fintype.card σ)) (j : ℕ) : (killBelow e (j + 1)).comp (killBelow e j) = killBelow e (j + 1)

theorem MultiplicativeBasisDeformations.OrbitDim.Pj_lt {k : Type u_1} [Field k] {σ : Type} [Fintype σ] [DecidableEq σ] (e : σ ≃ Fin (Fintype.card σ)) (j : ℕ) (hj : j < Fintype.card σ) : Pj e j < Pj e (j + 1)

theorem MultiplicativeBasisDeformations.OrbitDim.killBelow_top {k : Type u_1} [Field k] {σ : Type} [Fintype σ] [DecidableEq σ] (e : σ ≃ Fin (Fintype.card σ)) (f : MvPolynomial σ k) : (killBelow e (Fintype.card σ)) f = MvPolynomial.C ((MvPolynomial.eval 0) f)

theorem MultiplicativeBasisDeformations.OrbitDim.height_origin_ge {k : Type u_1} [Field k] {σ : Type} [Fintype σ] [DecidableEq σ] (e : σ ≃ Fin (Fintype.card σ)) : ↑(Fintype.card σ) ≤ (Pj e (Fintype.card σ)).height

The height of the origin is at least the number of variables.

theorem MultiplicativeBasisDeformations.OrbitDim.mem_Pj_top {k : Type u_1} [Field k] {σ : Type} [Fintype σ] [DecidableEq σ] (e : σ ≃ Fin (Fintype.card σ)) {f : MvPolynomial σ k} (hf : (MvPolynomial.eval 0) f = 0) : f ∈ Pj e (Fintype.card σ)

theorem MultiplicativeBasisDeformations.OrbitDim.dim_quot_ge {k : Type u_1} [Field k] {σ : Type} [Fintype σ] [DecidableEq σ] {F : ℕ} (f : Fin F → MvPolynomial σ k) (hf : ∀ (i : Fin F), (MvPolynomial.eval 0) (f i) = 0) : ↑(Fintype.card σ) ≤ ringKrullDim (MvPolynomial σ k ⧸ Ideal.span (Set.range f)) + ↑F

Step 1: the zero set of F polynomials vanishing at the origin has dimension at least N − F.

Step 2: charts of an orbit

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrbitDim.Coord {ι : Type} (d : ι → ℕ) {α : Type} (s t : α → ι) : Type

The coordinates of the representation space.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrbitDim.GC {ι : Type} (d : ι → ℕ) : Type

The coordinates of the group.

def MultiplicativeBasisDeformations.OrbitDim.mat {k : Type u_1} {ι : Type} {d : ι → ℕ} {α : Type} {s t : α → ι} (x : Coord d s t → k) (a : α) : Matrix (Fin (d (t a))) (Fin (d (s a))) k

The matrix of an arrow.

def MultiplicativeBasisDeformations.OrbitDim.act {k : Type u_1} [Field k] {ι : Type} {d : ι → ℕ} {α : Type} {s t : α → ι} (g : (v : ι) → GL (Fin (d v)) k) (x : Coord d s t → k) : Coord d s t → k

The action of ∏ GL_{d v}.

theorem MultiplicativeBasisDeformations.OrbitDim.mat_act {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (g : (v : ι) → GL (Fin (d v)) k) (x : Coord d s t → k) (a : α) : mat (act g x) a = ↑(g (t a)) * mat x a * ↑(g (s a))⁻¹

theorem MultiplicativeBasisDeformations.OrbitDim.act_act {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (g h : (v : ι) → GL (Fin (d v)) k) (x : Coord d s t → k) : act g (act h x) = act (g * h) x

theorem MultiplicativeBasisDeformations.OrbitDim.act_one {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (x : Coord d s t → k) : act 1 x = x

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrbitDim.Var {ι : Type} {d : ι → ℕ} (c : GC d) : Type

The variables of the chart c: the group coordinates other than c.

noncomputable def MultiplicativeBasisDeformations.OrbitDim.Gm (k : Type u_1) [Field k] {ι : Type} [DecidableEq ι] {d : ι → ℕ} (c : GC d) (v : ι) : Matrix (Fin (d v)) (Fin (d v)) (MvPolynomial (Var c) k)

The generic matrix of the chart, with 1 at c.

noncomputable def MultiplicativeBasisDeformations.OrbitDim.δ (k : Type u_1) [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) : MvPolynomial (Var c) k

The product of the determinants.

def MultiplicativeBasisDeformations.OrbitDim.gm {k : Type u_1} [Field k] {ι : Type} [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (v : ι) : Matrix (Fin (d v)) (Fin (d v)) k

The specialized matrices.

theorem MultiplicativeBasisDeformations.OrbitDim.map_Gm {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (v : ι) : (Gm k c v).map ⇑(MvPolynomial.eval pt) = gm c pt v

theorem MultiplicativeBasisDeformations.OrbitDim.eval_δ {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) : (MvPolynomial.eval pt) (δ k c) = ∏ v : ι, (gm c pt v).det

def MultiplicativeBasisDeformations.OrbitDim.pt0 {k : Type u_1} [Field k] {ι : Type} {d : ι → ℕ} (c : GC d) : Var c → k

A point of the chart where all specialized matrices have determinant one.

theorem MultiplicativeBasisDeformations.OrbitDim.det_gm_pt0 {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (v : ι) : (gm c (pt0 c) v).det = 1

theorem MultiplicativeBasisDeformations.OrbitDim.δ_ne_zero {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) : δ k c ≠ 0

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrbitDim.Rc {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) : Type u_1

The chart ring.

theorem MultiplicativeBasisDeformations.OrbitDim.isUnit_det {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (v : ι) : IsUnit ((algebraMap (MvPolynomial (Var c) k) (Rc c)) (Gm k c v).det)

noncomputable def MultiplicativeBasisDeformations.OrbitDim.Ψ (k : Type u_1) [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} {s t : α → ι} (c : GC d) (x : Coord d s t → k) : MvPolynomial (Coord d s t) k →ₐ[k] Rc c

The chart map of the orbit of x: x_a ↦ G_{t a} x_a G_{s a}⁻¹ for the generic matrices.

theorem MultiplicativeBasisDeformations.OrbitDim.isUnit_aeval_pow {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) (y : ↥(Submonoid.powers (δ k c))) : IsUnit ((MvPolynomial.aeval pt) ↑y)

noncomputable def MultiplicativeBasisDeformations.OrbitDim.ev {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) : Rc c →ₐ[k] k

Evaluation at a point of the chart.

theorem MultiplicativeBasisDeformations.OrbitDim.ev_algebraMap {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) (P : MvPolynomial (Var c) k) : (ev c pt hpt) ((algebraMap (MvPolynomial (Var c) k) (Rc c)) P) = (MvPolynomial.eval pt) P

theorem MultiplicativeBasisDeformations.OrbitDim.det_gm_ne {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) (v : ι) : (gm c pt v).det ≠ 0

def MultiplicativeBasisDeformations.OrbitDim.grp {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) (v : ι) : GL (Fin (d v)) k

The group element of a chart point.

theorem MultiplicativeBasisDeformations.OrbitDim.ev_unitInv {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) (v : ι) : (ev c pt hpt) ↑⋯.unit⁻¹ = (gm c pt v).det⁻¹

theorem MultiplicativeBasisDeformations.OrbitDim.map_ev_Gm {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) (v : ι) : ((Gm k c v).map ⇑(algebraMap (MvPolynomial (Var c) k) (Rc c))).map ⇑(ev c pt hpt) = gm c pt v

theorem MultiplicativeBasisDeformations.OrbitDim.ev_Ψ {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (c : GC d) (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0) (x : Coord d s t → k) (f : MvPolynomial (Coord d s t) k) : (ev c pt hpt) ((Ψ k c x) f) = (MvPolynomial.eval (act (grp c pt hpt) x)) f

Evaluating the chart map gives the action of the chart's group element.

instance MultiplicativeBasisDeformations.OrbitDim.instIsDomainRc {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) : IsDomain (Rc c)

theorem MultiplicativeBasisDeformations.OrbitDim.eq_zero_of_ev {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) [Infinite k] (r : Rc c) (h : ∀ (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0), (ev c pt hpt) r = 0) : r = 0

An element of the chart ring vanishing at all points is zero.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.OrbitDim.J (k : Type u_1) [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} {s t : α → ι} (c : GC d) (x : Coord d s t → k) : Ideal (MvPolynomial (Coord d s t) k)

The vanishing ideal of the chart image of the orbit of x.

instance MultiplicativeBasisDeformations.OrbitDim.J_isPrime {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} {s t : α → ι} (c : GC d) (x : Coord d s t → k) : (J k c x).IsPrime

theorem MultiplicativeBasisDeformations.OrbitDim.mem_J_iff {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (c : GC d) [Infinite k] (x : Coord d s t → k) (f : MvPolynomial (Coord d s t) k) : f ∈ J k c x ↔ ∀ (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0), (MvPolynomial.eval (act (grp c pt hpt) x)) f = 0

theorem MultiplicativeBasisDeformations.OrbitDim.exists_chart_pt {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (c : GC d) (g : (v : ι) → GL (Fin (d v)) k) (hc : ↑(g c.fst) c.snd.1 c.snd.2 ≠ 0) (x : Coord d s t → k) : ∃ (pt : Var c → k) (hpt : (MvPolynomial.eval pt) (δ k c) ≠ 0), act g x = act (grp c pt hpt) x

Charts cover the orbit: rescaling g to have entry one at c.

theorem MultiplicativeBasisDeformations.OrbitDim.exists_nonzero_entry {k : Type u_1} [Field k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (hd : ∃ (v : ι), 0 < d v) (g : (v : ι) → GL (Fin (d v)) k) : ∃ (c : GC d), ↑(g c.fst) c.snd.1 c.snd.2 ≠ 0

Every invertible family has a nonzero entry.

Step 3: the count

theorem MultiplicativeBasisDeformations.OrbitDim.card_var {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} (c : GC d) : Fintype.card (Var c) = Fintype.card (GC d) - 1

theorem MultiplicativeBasisDeformations.OrbitDim.dim_J_le {k : Type u_1} [Field k] [IsAlgClosed k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (c : GC d) (x : Coord d s t → k) : ringKrullDim (MvPolynomial (Coord d s t) k ⧸ J k c x) ≤ ↑(Fintype.card (GC d) - 1)

The chart image of an orbit has dimension at most D − 1.

theorem MultiplicativeBasisDeformations.OrbitDim.withBot_aux (a : WithBot ℕ∞) (N F D : ℕ) (h1 : ↑N ≤ a + ↑F) (h2 : D + F ≤ N) : ↑D ≤ a

theorem MultiplicativeBasisDeformations.OrbitDim.orbits_not_finite {k : Type u_1} [Field k] [IsAlgClosed k] {ι : Type} [Fintype ι] [DecidableEq ι] {d : ι → ℕ} {α : Type} [Fintype α] {s t : α → ι} (F : ℕ) (f : Fin F → MvPolynomial (Coord d s t) k) (hf0 : ∀ (i : Fin F), (MvPolynomial.eval 0) (f i) = 0) (hstab : ∀ (g : (v : ι) → GL (Fin (d v)) k) (x : Coord d s t → k), (∀ (i : Fin F), (MvPolynomial.eval x) (f i) = 0) → ∀ (i : Fin F), (MvPolynomial.eval (act g x)) (f i) = 0) (hd : ∃ (v : ι), 0 < d v) (hN : Fintype.card (GC d) + F ≤ Fintype.card (Coord d s t)) (S : Finset (Coord d s t → k)) (hS : ∀ (y : Coord d s t → k), (∀ (i : Fin F), (MvPolynomial.eval y) (f i) = 0) → ∃ x ∈ S, ∃ (g : (v : ι) → GL (Fin (d v)) k), y = act g x) : False

Lemma 8.8, geometric part: the zero set of F polynomials vanishing at the origin and stable under ∏ GL_{d v}, in N coordinates with N ≥ D + F, is not a finite union of orbits.