Building a symplectic form for each orbifold label

Proposition 2 of the orbifold-alphabet paper realises every label of its symplectic table by a pair of matrices R and a nondegenerate antisymmetric form J with Rᵀ J R = J. Three constructions:

• real type: R = ρ ⊗ I₂ and J = B ⊗ ε, with ρᵀ B ρ = B, B symmetric and ε antisymmetric;
• complex type: R = ρ ⊕ ρ̄ and J = [[0, I], [−I, 0]], with ρ unitary;
• quaternionic type: R = ρ, J = B (nothing to prove).

Main results

• kronecker_one_preserves: (ρ ⊗ I)ᵀ (B ⊗ ε) (ρ ⊗ I) = (ρᵀ B ρ) ⊗ ε = B ⊗ ε.
• kronecker_transpose_eq_neg: a symmetric B against an antisymmetric ε gives (B ⊗ ε)ᵀ = −(B ⊗ ε).
• fromBlocks_conj_preserves_J: for unitary ρ, ρ ⊕ ρ̄ preserves J; the off-diagonal blocks are ρᵀ ρ̄ = (ρᴴ ρ)ᵀ = I and ρ̄ᵀ ρ = ρᴴ ρ = I.

References

• C. Marín, The orbifold alphabet, Proposition 2 (prop:spbuild).

theorem OrbifoldAlphabet.SymplecticBuild.kronecker_one_preserves {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (ρ B : Matrix n n R) (ε : Matrix (Fin 2) (Fin 2) R) (h : ρ.transpose * B * ρ = B) : (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ 1).transpose * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) B ε * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ 1 = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) B ε

Real type: if ρ preserves the bilinear form B (ρᵀ B ρ = B), then ρ ⊗ I₂ preserves B ⊗ ε for every 2 × 2 matrix ε.

theorem OrbifoldAlphabet.SymplecticBuild.kronecker_transpose_eq_neg {R : Type u_1} {n : Type u_2} [CommRing R] (B : Matrix n n R) (ε : Matrix (Fin 2) (Fin 2) R) (hB : B.transpose = B) (hε : ε.transpose = -ε) : (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) B ε).transpose = -Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) B ε

Real type: a symmetric B against an antisymmetric ε gives an antisymmetric form B ⊗ ε.

theorem OrbifoldAlphabet.SymplecticBuild.fromBlocks_conj_preserves_J {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : Matrix n n ℂ) (h : ρ.conjTranspose * ρ = 1) : (Matrix.fromBlocks ρ 0 0 (ρ.map ⇑(starRingEnd ℂ))).transpose * Matrix.fromBlocks 0 1 (-1) 0 * Matrix.fromBlocks ρ 0 0 (ρ.map ⇑(starRingEnd ℂ)) = Matrix.fromBlocks 0 1 (-1) 0

Complex type: if ρ is unitary, ρ ⊕ ρ̄ preserves the standard symplectic form J = [[0, I], [−I, 0]], i.e. Rᵀ J R = J.