The product orbifold (S¹/ℤ₂)^k: the counts behind its semigroup

The affine semigroup of boundary conditions of (S¹/ℤ₂)^k (Part IX-B of the orbifold series) has one generator per label; a label is a choice of two parity bits per circle, and each of the 2^k fixed points (one reflection per circle) reads one bit per circle. This file proves the counts the paper uses and the arithmetic that decides it.

Main results

• marginal_injective, card_labels: distinct labels have distinct readouts, and there are 4^k labels, so the semigroup has n = 4^k generators.
• sum_choose_mul_two_pow: ∑ C(k, j) 2^j = 3^k, the number of faces of the boundary complex of the cross-polytope, which is dim S.
• fms_bound_met, fms_bound_violated: 4^k = 2·3^k − 2 for k = 1, 2 and 4^k > 2·3^k − 2 for k ≥ 3.
• not_completeIntersection_of_fms: Proposition 2 of the paper, with the cited Corollary 3.4 of Fischer, Morris and Shapiro (a complete intersection of dimension d ≥ 2 has at most 2d − 2 extreme rays) as a hypothesis.
• cut_vertices, edges_exceed: the count showing that (S¹/ℤ₂)^k is not a cut ideal for k ≥ 3 (equation (5)).
• not_cone_of_others, generator_extreme: a one-hot block vector of a family of distinct choices is not a non-negative combination of the others, so every generator of (S¹/ℤ₂)^k spans an extreme ray of the cone (the first step of the proof of Proposition 2).
• rank_circle, generators_eq, rank_generators: the generator matrix of (S¹/ℤ₂)^k is, up to reindexing, the k-th Kronecker power of a 4 × 4 matrix of rank 3, so it has rank 3^k: dim S = 3^k (the rank part of Proposition 2).

References

• C. Marín, An Affine Semigroup from Orbifold Boundary Conditions (Part IX-B), Zenodo (2026), doi:10.5281/zenodo.22254864, §8.
• K. G. Fischer, W. Morris, J. Shapiro, Affine semigroup rings that are complete intersections, Proc. Amer. Math. Soc. 125 (1997), Corollary 3.4.

@[reducible, inline]

abbrev OrbifoldProduct.Label (k : ℕ) : Type

A label of (S¹/ℤ₂)^k: two parity bits per circle (one for each of its two reflections).

Equations

• OrbifoldProduct.Label k = (Fin k → Bool × Bool)

@[reducible, inline]

abbrev OrbifoldProduct.FixedPoint (k : ℕ) : Type

A fixed point of (S¹/ℤ₂)^k: one of the two reflections of each circle.

Equations

• OrbifoldProduct.FixedPoint k = (Fin k → Bool)

def OrbifoldProduct.readout {k : ℕ} (t : Label k) (c : FixedPoint k) : Fin k → Bool

What a fixed point reads from a label: on each circle, the bit of the reflection it chose.

Equations

• OrbifoldProduct.readout t c i = if c i = true then (t i).2 else (t i).1

def OrbifoldProduct.marginal {k : ℕ} (t : Label k) : FixedPoint k → Fin k → Bool

The marginal datum of a label: its readout at every fixed point (the generator of the semigroup, as the indicator blocks of the paper encode it).

Equations

• OrbifoldProduct.marginal t c = OrbifoldProduct.readout t c

theorem OrbifoldProduct.marginal_injective (k : ℕ) : Function.Injective marginal

The two fixed points «all first reflections» and «all second reflections» already recover the label: distinct labels give distinct generators.

theorem OrbifoldProduct.card_labels (k : ℕ) : Fintype.card (Label k) = 4 ^ k

There are 4^k labels, hence n = 4^k generators.

theorem OrbifoldProduct.sum_choose_mul_two_pow (k : ℕ) : ∑ j ∈ Finset.range (k + 1), k.choose j * 2 ^ j = 3 ^ k

∑_{j ≤ k} C(k, j) 2^j = 3^k: the faces of the boundary complex of the k-dimensional cross-polytope, which is dim S for (S¹/ℤ₂)^k.

theorem OrbifoldProduct.fms_bound_met : 4 ^ 1 = 2 * 3 ^ 1 - 2 ∧ 4 ^ 2 = 2 * 3 ^ 2 - 2

At k = 1, 2 the extreme rays meet the bound 2d − 2 exactly.

theorem OrbifoldProduct.fms_bound_violated {k : ℕ} (hk : 3 ≤ k) : 2 * 3 ^ k - 2 < 4 ^ k

For k ≥ 3, 4^k > 2·3^k − 2: the extreme rays exceed the bound of Fischer, Morris and Shapiro.

theorem OrbifoldProduct.not_completeIntersection_of_fms {CI : Prop} {n d k : ℕ} (hfms : CI → n ≤ 2 * d - 2) (hn : n = 4 ^ k) (hd : d = 3 ^ k) (hk : 3 ≤ k) : ¬CI

Proposition 2, from the cited bound: if a complete intersection must have at most 2d − 2 extreme rays (Fischer–Morris–Shapiro, Corollary 3.4, taken as the hypothesis hfms), then with n = 4^k extreme rays and d = 3^k the semigroup of (S¹/ℤ₂)^k is not a complete intersection for any k ≥ 3.

theorem OrbifoldProduct.cut_vertices {m k : ℕ} (hm : 1 ≤ m) (h : 2 ^ (m - 1) = 4 ^ k) : m = 2 * k + 1

A cut ideal with 4^k coordinates needs a graph with 2^(m−1) = 4^k cuts, so m = 2k + 1 vertices.

theorem OrbifoldProduct.edges_exceed {k : ℕ} (hk : 3 ≤ k) : k * (2 * k + 1) < 3 ^ k - 1

Equation (5): for k ≥ 3 the 3^k − 1 edges a cut model would need exceed the k(2k+1) edges of the complete graph on 2k + 1 vertices, so (S¹/ℤ₂)^k is not a cut ideal.

def OrbifoldProduct.oneHot {B : Type u_1} {P : Type u_2} [DecidableEq P] (f : B → P) : B × P → ℚ

The one-hot block vector of a choice f : B → P: in block b, a 1 at position f b. A generator of the semigroup is the one-hot vector of its readouts (one indicator block per fixed point).

Equations

• OrbifoldProduct.oneHot f bp = if f bp.1 = bp.2 then 1 else 0

theorem OrbifoldProduct.sum_oneHot {B : Type u_1} {P : Type u_2} [Fintype B] [Fintype P] [DecidableEq P] (f : B → P) : ∑ bp : B × P, oneHot f bp = ↑(Fintype.card B)

theorem OrbifoldProduct.not_cone_of_others {ι : Type u_1} {B : Type u_2} {P : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype B] [Nonempty B] [Fintype P] [DecidableEq P] (v : ι → B → P) (hv : Function.Injective v) (i : ι) (c : ι → ℚ) (hc : ∀ (j : ι), 0 ≤ c j) (h : ∀ (bp : B × P), ∑ j ∈ Finset.univ.erase i, c j * oneHot (v j) bp = oneHot (v i) bp) : False

A one-hot block vector is not a non-negative combination of the other ones of a family of distinct choices: it spans an extreme ray of their cone. (Summing all coordinates forces the coefficients to add up to 1; in each block a vector with a positive coefficient must have its 1 where v i has it, so it is v i.)

theorem OrbifoldProduct.generator_extreme (k : ℕ) (t : Label k) (c : Label k → ℚ) (hc : ∀ (s : Label k), 0 ≤ c s) (h : ∀ (bp : FixedPoint k × (Fin k → Bool)), ∑ s ∈ Finset.univ.erase t, c s * oneHot (marginal s) bp = oneHot (marginal t) bp) : False

Every generator of (S¹/ℤ₂)^k spans an extreme ray: the one-hot vector of a label's readouts is not a non-negative combination of those of the other labels.

def OrbifoldProduct.circle : Matrix (Bool × Bool) (Bool × Bool) ℚ

One circle: rows are (fixed point, bit read), columns are labels (t₁, t₂).

Equations

• OrbifoldProduct.circle cb t = if (if cb.1 = true then t.2 else t.1) = cb.2 then 1 else 0

def OrbifoldProduct.circleRows : Matrix (Fin 3) (Bool × Bool) ℚ

Rows (false, false), (false, true), (true, false) of circle.

Equations

• OrbifoldProduct.circleRows = OrbifoldProduct.circle.submatrix ![(false, false), (false, true), (true, false)] id

def OrbifoldProduct.circleCoeffs : Matrix (Bool × Bool) (Fin 3) ℚ

Coefficients of the rows of circle in circleRows: row (true, true) is the first two minus the third.

Equations

• OrbifoldProduct.circleCoeffs (false, false) = ![1, 0, 0]
• OrbifoldProduct.circleCoeffs (false, true) = ![0, 1, 0]
• OrbifoldProduct.circleCoeffs (true, false) = ![0, 0, 1]
• OrbifoldProduct.circleCoeffs (true, true) = ![1, 1, -1]

theorem OrbifoldProduct.circle_eq_mul : circle = circleCoeffs * circleRows

theorem OrbifoldProduct.rank_circle : circle.rank = 3

def OrbifoldProduct.generators (k : ℕ) : Matrix (FixedPoint k × (Fin k → Bool)) (Label k) ℚ

The generator matrix of (S¹/ℤ₂)^k: column t is the one-hot vector of the readouts of label t.

Equations

• OrbifoldProduct.generators k cb t = OrbifoldProduct.oneHot (OrbifoldProduct.marginal t) cb

theorem OrbifoldProduct.generators_eq (k : ℕ) : generators k = (Matrix.piKronecker k circle).submatrix ⇑(Equiv.arrowProdEquivProdArrow (Fin k) (fun (x : Fin k) => Bool) fun (x : Fin k) => Bool).symm ⇑(Equiv.refl (Fin k → Bool × Bool))

theorem OrbifoldProduct.rank_generators (k : ℕ) : (generators k).rank = 3 ^ k

dim S = 3^k: the generators of (S¹/ℤ₂)^k span a space of dimension 3^k.