The standard orthosymplectic super vector space

The concrete model of §5.1 of the accompanying paper: the super vector space with even part Fin k → ℂ and odd part Fin (2ℓ) → ℂ, carrying the pinned Regts–Sevenster form — orthonormal on the even part, and on the odd part the antisymmetric form with b (f m) (f (m + ℓ)) = 1 = −b (f (m + ℓ)) (f m). The dual vectors g i and the partner index calculus reuse oddPartner and oddPartnerSign from the Definition 5 machinery, so the two sides of the Contraction–Expansion Lemma speak the same language.

The odd basis is named as in Regts–Sevenster, f i and g i; the accompanying paper writes ξ i and η i for the same vectors, f being reserved there for the graph parameter.

noncomputable def RS.stdSuperPair (k ℓ : ℕ) : SuperVect

The standard super vector space with even dimension k and odd dimension 2ℓ.

Equations

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

noncomputable def RS.stdE (k : ℕ) (i : Fin k) : Fin k → ℂ

The standard even basis vectors e i.

Equations

• RS.stdE k i = Pi.single i 1

noncomputable def RS.stdF (ℓ : ℕ) (i : Fin (2 * ℓ)) : Fin (2 * ℓ) → ℂ

The standard odd basis vectors f i.

Equations

• RS.stdF ℓ i = Pi.single i 1

noncomputable def RS.stdFormEven (k : ℕ) (x y : Fin k → ℂ) : ℂ

The even part of the standard form: the orthonormal pairing.

Equations

• RS.stdFormEven k x y = ∑ i : Fin k, x i * y i

noncomputable def RS.stdFormOdd (ℓ : ℕ) (x y : Fin (2 * ℓ) → ℂ) : ℂ

The odd part of the standard form: the antisymmetric pairing with b (f m) (f (m + ℓ)) = 1 for m ≤ ℓ and all other basis values forced by antisymmetry.

Equations

• RS.stdFormOdd ℓ x y = ∑ i : Fin (2 * ℓ), -↑(RS.oddPartnerSign ℓ i) * x i * y (RS.oddPartner ℓ i)

noncomputable def RS.stdG (ℓ : ℕ) (i : Fin (2 * ℓ)) : Fin (2 * ℓ) → ℂ

The Regts–Sevenster dual odd vectors: g i = −f (i + ℓ) for i < ℓ and g i = f (i − ℓ) otherwise.

Equations

• RS.stdG ℓ i = ↑(RS.oddPartnerSign ℓ i) • RS.stdF ℓ (RS.oddPartner ℓ i)

theorem RS.stdFormEven_stdE (k : ℕ) (i j : Fin k) : stdFormEven k (stdE k i) (stdE k j) = if i = j then 1 else 0

The even form is orthonormal on the standard basis.

theorem RS.stdFormOdd_stdF (ℓ : ℕ) (i j : Fin (2 * ℓ)) : stdFormOdd ℓ (stdF ℓ i) (stdF ℓ j) = if j = oddPartner ℓ i then -↑(oddPartnerSign ℓ i) else 0

The odd form on the standard basis: −oddPartnerSign at the partner index and zero elsewhere.

theorem RS.stdFormOdd_antisymm (ℓ : ℕ) (x y : Fin (2 * ℓ) → ℂ) : stdFormOdd ℓ x y = -stdFormOdd ℓ y x

The odd form is antisymmetric.

theorem RS.stdFormOdd_stdF_stdG (ℓ : ℕ) (i j : Fin (2 * ℓ)) : stdFormOdd ℓ (stdF ℓ i) (stdG ℓ j) = if i = j then -1 else 0

The companion pairing identity: b (f i) (g j) = −δ_{ij}.

theorem RS.sum_stdFormEven_diag (k : ℕ) : ∑ i : Fin k, stdFormEven k (stdE k i) (stdE k i) = ↑k

The even trace of the copairing: Σ_i b(e_i, e_i) = k.

theorem RS.sum_stdFormOdd_diag (ℓ : ℕ) : ∑ i : Fin (2 * ℓ), stdFormOdd ℓ (stdF ℓ i) (stdG ℓ i) = -(2 * ↑ℓ)

The odd trace of the copairing: Σ_i b(f_i, g_i) = −2ℓ; together with the even part this is b(C) = k − 2ℓ, the value of a free circle.

theorem RS.stdFormEven_stdE_left (k : ℕ) (j : Fin k) (x : Fin k → ℂ) : stdFormEven k (stdE k j) x = x j

The even form against a basis vector reads off the coordinate.

theorem RS.stdFormOdd_stdG_left (ℓ : ℕ) (j : Fin (2 * ℓ)) (x : Fin (2 * ℓ) → ℂ) : stdFormOdd ℓ (stdG ℓ j) x = x j

The odd form against a dual basis vector reads off the coordinate.

theorem RS.sum_stdFormEven_smul (k : ℕ) (x : Fin k → ℂ) : ∑ i : Fin k, stdFormEven k (stdE k i) x • stdE k i = x

The even contraction identity (accompanying paper, §5.2): contracting the even copairing through the form is the identity.