The ordered sign cover of an integral lattice

Let B : Matrix I I ℤ be the Gram matrix of the lattice Q = I → ℤ in the basis indexed by a linearly ordered finite set I, for instance the Cartan matrix of a simply laced Dynkin diagram with its vertices ordered. Keeping only the strictly lower triangular entries of B gives a bilinear form

β(a, b) = ∑_{j < i} a i * B i j * b j

on Q, and its sign ε(a, b) = (-1) ^ β(a, b) is bimultiplicative, hence a factor set of Q with values in ℤˣ. The central extension 1 → ℤˣ → Q̂ → Q → 1 it builds is the ordered sign cover of Q: its elements are pairs of a lattice vector and a sign, multiplied by (a, s) * (b, t) = (a + b, s * t * ε(a, b)).

For a simply laced diagram, -B i j is the number of bonds between distinct vertices i and j, so ε(a, b) is the parity of the bonds pairing a later coordinate of a with an earlier one of b. The point of the cover is its commutator formula: when B is symmetric with even diagonal, the commutator of two elements of Q̂ lying over a and b is τ ^ (a ⬝ᵥ B *ᵥ b), a power of the central sign τ = (0, -1) (Matrix.commutatorElement_signCover). This is the sign input of the Frenkel--Kac construction of a simply laced Lie algebra over ℤ, whose root vectors are indexed by lifts of roots to Q̂. The bracket Matrix.ShellLieAlgebra, in TauCeti.Algebra.Lie.NormTwoShell.Basic, uses this cocycle on root vectors indexed by the section a ↦ (a, 1) instead, so it is not the lifted-generator presentation. The section a ↦ (a, 1) is a homomorphism exactly when every strictly lower entry of B is even (Matrix.forall_canonicalSection_signFactorSet_mul_iff); for a simply laced diagram this means exactly that the diagram has no bonds, which is proved in TauCeti.LinearAlgebra.Matrix.OrderedSignCover.SimplyLaced.

The group structure, the inclusion of ℤˣ, the projection to Multiplicative Q, the exactness of 1 → ℤˣ → Q̂ → Q → 1, the section a ↦ (a, 1) and the centrality of ℤˣ all come from the general factor-set construction TauCeti.FactorSet.Extension for the trivial action of Q on ℤˣ; this file supplies the sign cocycle and the facts specific to it.

Main definitions

• Matrix.orderedSignForm B: the bilinear form of the strictly lower triangular part of B.
• Matrix.orderedSign B: its sign ε, as a bimultiplicative map on Multiplicative Q.
• Matrix.signFactorSet B: ε as a factor set for the trivial action of Q on ℤˣ.
• Matrix.SignCover B: the central extension Q̂ of Q by ℤˣ it builds.
• Matrix.SignCover.tau B: the central sign τ, the image of -1 : ℤˣ in Q̂.

Main results

• Matrix.orderedSignForm_add_orderedSignForm_swap: for symmetric B, the symmetrization of the ordered form is the Gram pairing with its diagonal terms removed.
• Matrix.even_orderedSignForm_add_orderedSignForm_swap_sub: for symmetric B with even diagonal, orderedSignForm B a b + orderedSignForm B b a and a ⬝ᵥ B *ᵥ b have the same parity.
• Matrix.orderedSign_div_orderedSign_swap: for symmetric B with even diagonal, ε(a, b) / ε(b, a) = (-1) ^ (a ⬝ᵥ B *ᵥ b).
• Matrix.SignCover.inl_range_le_center: the copy of ℤˣ in Q̂ is central, the hypothesis under which Q̂ admits character twists.
• Matrix.SignCover.inv_canonicalSection: the inverse lift ⟨1, a⟩⁻¹ = ε(a, a) ⟨1, -a⟩.
• Matrix.commutatorElement_signCover: the commutator formula in Q̂.
• Matrix.forall_canonicalSection_signFactorSet_mul_iff: the section a ↦ (a, 1) is a homomorphism exactly when all strictly lower entries of B are even.

References

• I. B. Frenkel and V. G. Kac, Basic representations of affine Lie algebras and dual resonance models, Invent. Math. 62 (1980), 23--66.
• V. G. Kac, Infinite dimensional Lie algebras, third edition, Cambridge University Press (1990), §7.8.

noncomputable def Matrix.orderedSignForm {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : LinearMap.BilinForm ℤ (I → ℤ)

The ordered form of an integer matrix: the bilinear form on I → ℤ of the strictly lower triangular part of B for the order of I, orderedSignForm B a b = ∑_{j < i} a i * B i j * b j. Its sign is the factor set Matrix.signFactorSet B.

theorem Matrix.orderedSignForm_apply {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (a b : I → ℤ) : (B.orderedSignForm a) b = ∑ i : I, ∑ j : I, if j < i then a i * B i j * b j else 0

@[simp]

theorem Matrix.orderedSignForm_single_single {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (i j : I) : (B.orderedSignForm (Pi.single i 1)) (Pi.single j 1) = if j < i then B i j else 0

On basis vectors the ordered form reads off the strictly lower triangular entries of B.

theorem Matrix.orderedSignForm_add_orderedSignForm_swap {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (hB : B.IsSymm) (a b : I → ℤ) : (B.orderedSignForm a) b + (B.orderedSignForm b) a + ∑ i : I, a i * B i i * b i = a ⬝ᵥ B.mulVec b

Symmetrizing the ordered form. For a symmetric matrix B, adding the ordered form to its transpose recovers the Gram pairing a ⬝ᵥ B *ᵥ b with its diagonal terms removed: each off-diagonal pair i ≠ j is counted once by whichever of the two forms sees j < i.

noncomputable def Matrix.orderedSign {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : Multiplicative (I → ℤ) →* Multiplicative (I → ℤ) →* ℤˣ

The ordered sign of an integer matrix: ε(a, b) = (-1) ^ orderedSignForm B a b, written Int.negOnePow (orderedSignForm B a b), as a map on Multiplicative (I → ℤ) that is multiplicative in each variable. This is the factor set of the ordered sign cover Matrix.SignCover B.

@[simp]

theorem Matrix.orderedSign_apply {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (a b : Multiplicative (I → ℤ)) : (B.orderedSign a) b = ((B.orderedSignForm (Multiplicative.toAdd a)) (Multiplicative.toAdd b)).negOnePow

theorem Matrix.even_orderedSignForm_add_orderedSignForm_swap_sub {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (hB : B.IsSymm) (hdiag : ∀ (i : I), Even (B i i)) (a b : I → ℤ) : Even ((B.orderedSignForm a) b + (B.orderedSignForm b) a - a ⬝ᵥ B.mulVec b)

The commutator parity. For a symmetric matrix B with even diagonal, the ordered form and its transpose add up to the Gram pairing modulo 2.

theorem Matrix.orderedSign_div_orderedSign_swap {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (hB : B.IsSymm) (hdiag : ∀ (i : I), Even (B i i)) (a b : Multiplicative (I → ℤ)) : (B.orderedSign a) b / (B.orderedSign b) a = (Multiplicative.toAdd a ⬝ᵥ B.mulVec (Multiplicative.toAdd b)).negOnePow

The commutator sign. For a symmetric matrix B with even diagonal, the ratio of the two ordered signs of a and b is the sign of their Gram pairing.

noncomputable def Matrix.signFactorSet {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : TauCeti.FactorSet (Multiplicative (I → ℤ)) ℤˣ

The ordered sign factor set of an integer matrix: the bimultiplicative ordered sign Matrix.orderedSign B as a factor set of Multiplicative (I → ℤ) with values in ℤˣ, for the trivial action.

@[simp]

theorem Matrix.signFactorSet_apply {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (p : Multiplicative (I → ℤ) × Multiplicative (I → ℤ)) : B.signFactorSet p = (B.orderedSign p.1) p.2

@[reducible, inline]

abbrev Matrix.SignCover {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : Type u_1

The ordered sign cover Q̂ of the lattice Q = I → ℤ with Gram matrix B: the central extension 1 → ℤˣ → Q̂ → Q → 1 built from the ordered sign factor set. An element is a pair of a sign x.left and a lattice vector x.right, and x * y = ⟨x.left * y.left * ε(x.right, y.right), x.right * y.right⟩. The inclusion of ℤˣ, the projection to Multiplicative Q and the section a ↦ ⟨1, a⟩ are TauCeti.FactorSet.inl, TauCeti.FactorSet.rightHom and TauCeti.FactorSet.canonicalSection of Matrix.signFactorSet B, and (Matrix.signFactorSet B).groupExtension packages them as a GroupExtension. The image of ℤˣ is central by TauCeti.FactorSet.inl_range_le_center, the action being trivial.

noncomputable def Matrix.SignCover.tau {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : B.SignCover

The central sign τ = ⟨-1, 1⟩ of the ordered sign cover: the image of -1 : ℤˣ, an element of order 2 in the center.

@[simp]

theorem Matrix.SignCover.tau_left {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : (tau B).left = -1

@[simp]

theorem Matrix.SignCover.tau_right {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : (tau B).right = 1

@[simp]

theorem Matrix.SignCover.tau_mul_self {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : tau B * tau B = 1

theorem Matrix.SignCover.tau_ne_one {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : tau B ≠ 1

theorem Matrix.SignCover.tau_mem_center {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : tau B ∈ Subgroup.center B.SignCover

theorem Matrix.SignCover.inl_range_le_center {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : B.signFactorSet.groupExtension.inl.range ≤ Subgroup.center B.SignCover

The copy of ℤˣ in the ordered sign cover is central.

theorem Matrix.SignCover.inv_canonicalSection {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (a : Multiplicative (I → ℤ)) : (B.signFactorSet.canonicalSection a)⁻¹ = B.signFactorSet.inl ((B.orderedSign a) a) * B.signFactorSet.canonicalSection a⁻¹

The inverse lift in the ordered sign cover: the inverse of the section value ⟨1, a⟩ lies over -a with the sign ε(a, a), that is, ⟨1, a⟩⁻¹ = ε(a, a) ⟨1, -a⟩.

theorem Matrix.commutatorElement_signCover {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (hB : B.IsSymm) (hdiag : ∀ (i : I), Even (B i i)) (x y : B.SignCover) : ⁅x, y⁆ = SignCover.tau B ^ (Multiplicative.toAdd x.right ⬝ᵥ B.mulVec (Multiplicative.toAdd y.right))

The commutator formula of the ordered sign cover. For a symmetric matrix B with even diagonal, two elements of the cover lying over a and b commute up to the power τ ^ (a ⬝ᵥ B *ᵥ b) of the central sign given by their Gram pairing, whatever signs they carry.

theorem Matrix.forall_canonicalSection_signFactorSet_mul_iff {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) : (∀ (a b : Multiplicative (I → ℤ)), B.signFactorSet.canonicalSection (a * b) = B.signFactorSet.canonicalSection a * B.signFactorSet.canonicalSection b) ↔ ∀ (i j : I), j < i → Even (B i j)

The canonical section of the ordered sign cover is a homomorphism exactly when every strictly lower triangular entry of B is even, that is, exactly when the ordered sign is trivial.