The ordered sign cover of a simply laced lattice

For a symmetric simply laced Gram matrix B (Matrix.IsSimplyLaced), such as the Cartan matrix of a simply laced Dynkin diagram, the off-diagonal entries are 0 or -1, the negative of the number of bonds. The canonical section a ↦ (a, 1) of the ordered sign cover Matrix.SignCover B is a homomorphism exactly when every strictly lower entry of B is even (Matrix.forall_canonicalSection_signFactorSet_mul_iff), so here exactly when the diagram has no bonds.

This is kept apart from TauCeti.LinearAlgebra.Matrix.OrderedSignCover so that the general cover does not import the theory of Cartan matrices.

Main results

• Matrix.forall_canonicalSection_signFactorSet_mul_iff_of_isSimplyLaced: for a symmetric simply laced B, the section a ↦ (a, 1) is a homomorphism exactly when B is diagonal.

theorem Matrix.forall_canonicalSection_signFactorSet_mul_iff_of_isSimplyLaced {I : Type u_1} [Fintype I] [LinearOrder I] (B : Matrix I I ℤ) (hB : B.IsSymm) (hsl : B.IsSimplyLaced) : (∀ (a b : Multiplicative (I → ℤ)), B.signFactorSet.canonicalSection (a * b) = B.signFactorSet.canonicalSection a * B.signFactorSet.canonicalSection b) ↔ ∀ (i j : I), i ≠ j → B i j = 0

For a simply laced Gram matrix, the canonical section of the ordered sign cover is a homomorphism exactly when the diagram has no bonds. Here B is symmetric and simply laced, with off-diagonal entries 0 or -1, the negative of the number of bonds, as for the Cartan matrix of a simply laced Dynkin diagram.