The norm-two shell of a simply laced Gram matrix

Let B be an integer matrix indexed by a finite type I, read as the Gram matrix of the lattice Q = I → ℤ with the pairing ⟪a, b⟫ = a ⬝ᵥ B *ᵥ b. Its norm-two shell is the set Φ = {a | ⟪a, a⟫ = 2} (Matrix.normTwoShell). When B is the Cartan matrix of a simply laced Dynkin diagram, possibly disconnected, Q is the root lattice in simple-root coordinates and Φ is its set of roots; the coordinate vector Pi.single i 1 is the simple root αᵢ.

The file develops the elementary theory of Φ in layers of hypotheses.

• For symmetric B, ⟪a + b, a + b⟫ = ⟪a, a⟫ + ⟪b, b⟫ + 2⟪a, b⟫, so for a, b ∈ Φ the sum a + b lies in Φ exactly when ⟪a, b⟫ = -1, and a - b exactly when ⟪a, b⟫ = 1; likewise the reflection x ↦ x - ⟪x, a⟫ a in a vector of Φ preserves Φ.
• For positive definite B, two vectors of Φ pair to 2 exactly when they are equal and to -2 exactly when they are opposite, and otherwise to -1, 0 or 1. The shell is finite.
• If in addition the diagonal is even, every nonzero vector has norm at least two. When also the off-diagonal entries are nonpositive, as for a simply laced Cartan matrix, every vector of Φ has coefficients of one sign: writing a = a⁺ - a⁻ with disjointly supported nonnegative parts, ⟪a⁺, a⁻⟫ ≤ 0, so two nonzero parts would give ⟪a, a⟫ ≥ 4.
• For positive definite B with diagonal 2 alone, a nonnegative vector of Φ that is not simple pairs to 1 with some simple root αᵢ, and a - αᵢ is again a nonnegative vector of Φ, of height one less. This is the height induction Matrix.PosDef.normTwoShell_nonneg_induction: every nonnegative vector of Φ is reached from a simple root by adding simple roots one at a time without leaving Φ.

These are the facts about the root set that the integral Chevalley lattice of a simply laced diagram is built on: its root vectors are indexed by Φ, and its bracket on root vectors is nonzero exactly in the cases a + b ∈ Φ and a = -b isolated here. The nonzero height also gives a single integral vector separating all shell vectors by the pairing, invariant under a specified diagram permutation. Mathlib's Matrix.cramer constructs it, and Matrix.mulVec_cramer identifies its root pairings with determinant times height.

Main definitions

• Matrix.normTwoShell: the vectors of norm two of an integer Gram matrix.
• Matrix.normTwoShellCongr: the bijection of norm-two shells induced by a relabelling of the vertices.
• Matrix.normTwoShellEquivOfIsometry: the bijection of norm-two shells induced by a linear isometry of Gram lattices.

Main results

• Matrix.IsSymm.add_mem_normTwoShell_iff: for a, b ∈ Φ, a + b ∈ Φ ↔ ⟪a, b⟫ = -1.
• Matrix.IsSymm.dotProduct_mulVec_add_add_of_mem_normTwoShell: the norm of a + b + c for a, b, c ∈ Φ in terms of their pairings.
• Matrix.PosDef.dotProduct_mulVec_eq_two_iff and Matrix.PosDef.dotProduct_mulVec_eq_neg_two_iff: for a, b ∈ Φ, ⟪a, b⟫ = 2 ↔ a = b and ⟪a, b⟫ = -2 ↔ a = -b.
• Matrix.PosDef.dotProduct_mulVec_le_one and Matrix.PosDef.neg_one_le_dotProduct_mulVec: two vectors of Φ that are neither equal nor opposite pair into {-1, 0, 1}.
• Matrix.PosDef.finite_normTwoShell: the shell of a positive definite matrix is finite.
• Matrix.PosDef.nonneg_or_nonpos_of_mem_normTwoShell: with nonpositive off-diagonal entries, every vector of Φ is nonnegative or nonpositive.
• Matrix.PosDef.exists_invariant_pairing_ne_zero: an invariant integral vector pairs nontrivially with every shell vector.
• Matrix.PosDef.exists_sub_single_mem_normTwoShell: a positive root that is not simple has a simple root whose subtraction leaves a positive root.
• Matrix.PosDef.normTwoShell_nonneg_induction: the height induction principle for positive roots.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter VI, §1.6 and §4.
• V. G. Kac, Infinite dimensional Lie algebras, third edition, Proposition 5.10 and §7.8.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §10.2.

def Matrix.normTwoShell {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) : Set (I → ℤ)

The norm-two shell of an integer Gram matrix B: the integer vectors a with a ⬝ᵥ B *ᵥ a = 2. For the Cartan matrix of a simply laced Dynkin diagram, read in simple-root coordinates, these are the roots.

theorem Matrix.mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} : a ∈ B.normTwoShell ↔ a ⬝ᵥ B.mulVec a = 2

@[simp]

theorem Matrix.neg_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} : -a ∈ B.normTwoShell ↔ a ∈ B.normTwoShell

The norm-two shell is symmetric under negation.

theorem Matrix.smul_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} {ζ : ℤ} (hζ : ζ * ζ = 1) (ha : a ∈ B.normTwoShell) : ζ • a ∈ B.normTwoShell

The norm-two shell is stable under multiplication by a sign ζ, an integer with ζ * ζ = 1.

theorem Matrix.ne_zero_of_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} (ha : a ∈ B.normTwoShell) : a ≠ 0

A vector of the norm-two shell is nonzero.

@[simp]

theorem Matrix.single_mem_normTwoShell_iff {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [DecidableEq I] {i : I} : Pi.single i 1 ∈ B.normTwoShell ↔ B i i = 2

A coordinate vector lies in the norm-two shell exactly when the diagonal entry is 2.

theorem Matrix.single_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [DecidableEq I] {i : I} (hi : B i i = 2) : Pi.single i 1 ∈ B.normTwoShell

A coordinate vector lies in the norm-two shell when the diagonal entry is 2.

theorem Matrix.span_normTwoShell_eq_top_of_diagonal_eq_two {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (hdiag : ∀ (i : I), B i i = 2) : Submodule.span ℤ B.normTwoShell = ⊤

Diagonal entries equal to two put a basis in the norm-two shell, so the shell spans.

Symmetric Gram matrices

theorem Matrix.IsSymm.add_mem_normTwoShell_iff {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a b : I → ℤ} (hB : B.IsSymm) (ha : a ∈ B.normTwoShell) (hb : b ∈ B.normTwoShell) : a + b ∈ B.normTwoShell ↔ a ⬝ᵥ B.mulVec b = -1

The sum of two vectors of the norm-two shell lies in it exactly when they pair to -1.

theorem Matrix.IsSymm.sub_mem_normTwoShell_iff {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a b : I → ℤ} (hB : B.IsSymm) (ha : a ∈ B.normTwoShell) (hb : b ∈ B.normTwoShell) : a - b ∈ B.normTwoShell ↔ a ⬝ᵥ B.mulVec b = 1

The difference of two vectors of the norm-two shell lies in it exactly when they pair to 1.

theorem Matrix.IsSymm.dotProduct_mulVec_add_add_of_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a b : I → ℤ} (hB : B.IsSymm) {c : I → ℤ} (ha : a ∈ B.normTwoShell) (hb : b ∈ B.normTwoShell) (hc : c ∈ B.normTwoShell) : (a + b + c) ⬝ᵥ B.mulVec (a + b + c) = 6 + 2 * (a ⬝ᵥ B.mulVec b + b ⬝ᵥ B.mulVec c + c ⬝ᵥ B.mulVec a)

The norm of the sum of three vectors of the norm-two shell, in terms of their pairings.

theorem Matrix.IsSymm.sub_smul_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a x : I → ℤ} (hB : B.IsSymm) (ha : a ∈ B.normTwoShell) (hx : x ∈ B.normTwoShell) : x - (x ⬝ᵥ B.mulVec a) • a ∈ B.normTwoShell

The reflection in a vector of the norm-two shell maps the shell to itself.

Positive definite Gram matrices

theorem Matrix.PosDef.two_le_dotProduct_mulVec_self {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} (hB : B.PosDef) (hev : ∀ (i : I), Even (B i i)) (ha : a ≠ 0) : 2 ≤ a ⬝ᵥ B.mulVec a

For an even diagonal, every nonzero vector has norm at least two.

theorem Matrix.PosDef.dotProduct_mulVec_eq_two_iff {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a b : I → ℤ} (hB : B.PosDef) (ha : a ∈ B.normTwoShell) (hb : b ∈ B.normTwoShell) : a ⬝ᵥ B.mulVec b = 2 ↔ a = b

Two vectors of the norm-two shell pair to 2 exactly when they are equal.

theorem Matrix.PosDef.dotProduct_mulVec_eq_neg_two_iff {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a b : I → ℤ} (hB : B.PosDef) (ha : a ∈ B.normTwoShell) (hb : b ∈ B.normTwoShell) : a ⬝ᵥ B.mulVec b = -2 ↔ a = -b

Two vectors of the norm-two shell pair to -2 exactly when they are opposite.

theorem Matrix.PosDef.dotProduct_mulVec_le_one {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a b : I → ℤ} (hB : B.PosDef) (ha : a ∈ B.normTwoShell) (hb : b ∈ B.normTwoShell) (hab : a ≠ b) : a ⬝ᵥ B.mulVec b ≤ 1

Two distinct vectors of the norm-two shell pair to at most 1.

theorem Matrix.PosDef.neg_one_le_dotProduct_mulVec {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a b : I → ℤ} (hB : B.PosDef) (ha : a ∈ B.normTwoShell) (hb : b ∈ B.normTwoShell) (hab : a ≠ -b) : -1 ≤ a ⬝ᵥ B.mulVec b

Two non-opposite vectors of the norm-two shell pair to at least -1.

theorem Matrix.PosDef.finite_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} (hB : B.PosDef) : B.normTwoShell.Finite

The norm-two shell of a positive definite integer matrix is finite.

Even diagonal and nonpositive off-diagonal entries

theorem Matrix.PosDef.nonneg_or_nonpos_of_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} (hB : B.PosDef) (hev : ∀ (i : I), Even (B i i)) (hoff : ∀ (i j : I), i ≠ j → B i j ≤ 0) (ha : a ∈ B.normTwoShell) : 0 ≤ a ∨ a ≤ 0

Every vector of the norm-two shell has coefficients of one sign, for a positive definite Gram matrix with even diagonal and nonpositive off-diagonal entries, such as a simply laced Cartan matrix.

theorem Matrix.PosDef.sum_ne_zero_of_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} (hB : B.PosDef) (hev : ∀ (i : I), Even (B i i)) (hoff : ∀ (i j : I), i ≠ j → B i j ≤ 0) (ha : a ∈ B.normTwoShell) : ∑ i : I, a i ≠ 0

A norm-two vector has nonzero total simple-root coordinate: its coordinates have one sign and do not all vanish.

theorem Matrix.PosDef.exists_invariant_pairing_ne_zero {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} (hB : B.PosDef) (hev : ∀ (i : I), Even (B i i)) (hoff : ∀ (i j : I), i ≠ j → B i j ≤ 0) (σ : Equiv.Perm I) (hσ : (reindex σ σ) B = B) : ∃ (h : I → ℤ), h ∘ ⇑(Equiv.symm σ) = h ∧ ∀ (a : ↑B.normTwoShell), h ⬝ᵥ B.mulVec ↑a ≠ 0

A permutation preserving the Gram matrix fixes an integral vector pairing nontrivially with every norm-two vector.

Positive roots and height induction, for diagonal 2

theorem Matrix.PosDef.exists_sub_single_mem_normTwoShell {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} [DecidableEq I] (hB : B.PosDef) (hdiag : ∀ (i : I), B i i = 2) (ha : a ∈ B.normTwoShell) (hpos : 0 ≤ a) (hsimple : ∀ (i : I), a ≠ Pi.single i 1) : ∃ (i : I), a ⬝ᵥ B.mulVec (Pi.single i 1) = 1 ∧ a - Pi.single i 1 ∈ B.normTwoShell ∧ 0 ≤ a - Pi.single i 1

A positive root that is not simple has a simple root whose subtraction leaves a positive root. For a positive definite Gram matrix with diagonal 2, a nonnegative vector a of the norm-two shell other than every coordinate vector pairs to 1 with some coordinate vector αᵢ, and a - αᵢ is again a nonnegative vector of the shell.

theorem Matrix.PosDef.normTwoShell_nonneg_induction {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} [DecidableEq I] (hB : B.PosDef) (hdiag : ∀ (i : I), B i i = 2) {motive : (I → ℤ) → Prop} (simple : ∀ (i : I), motive (Pi.single i 1)) (add : ∀ (a : I → ℤ) (i : I), a ∈ B.normTwoShell → 0 ≤ a → a + Pi.single i 1 ∈ B.normTwoShell → motive a → motive (a + Pi.single i 1)) (ha : a ∈ B.normTwoShell) (hpos : 0 ≤ a) : motive a

Height induction on positive roots. Let B be a positive definite Gram matrix with diagonal 2, such as the Cartan matrix of a simply laced Dynkin diagram. A property holding at every simple root Pi.single i 1, and passing from a nonnegative vector a of the norm-two shell to a + Pi.single i 1 whenever the latter is again in the shell, holds at every nonnegative vector of the shell.

theorem Matrix.comp_equiv_symm_mem_normTwoShell_reindex_iff {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} {J : Type u_2} [Fintype J] (e : I ≃ J) : a ∘ ⇑e.symm ∈ ((reindex e e) B).normTwoShell ↔ a ∈ B.normTwoShell

A relabelled vector lies in the norm-two shell of the relabelled matrix exactly when the vector lies in the norm-two shell of the matrix.

def Matrix.normTwoShellCongr {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {J : Type u_2} [Fintype J] {e : I ≃ J} {B' : Matrix J J ℤ} (he : (reindex e e) B = B') : ↑B.normTwoShell ≃ ↑B'.normTwoShell

The norm-two shell of a relabelled Gram matrix: for a relabelling e : I ≃ J of the vertices of B with B.reindex e e = B', the bijection a ↦ a ∘ e.symm from the norm-two shell of B to that of B'.

@[simp]

theorem Matrix.coe_normTwoShellCongr_apply {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {J : Type u_2} [Fintype J] {e : I ≃ J} {B' : Matrix J J ℤ} (he : (reindex e e) B = B') (a : ↑B.normTwoShell) : ↑((normTwoShellCongr he) a) = ↑a ∘ ⇑e.symm

@[simp]

theorem Matrix.coe_normTwoShellCongr_symm_apply {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {J : Type u_2} [Fintype J] {e : I ≃ J} {B' : Matrix J J ℤ} (he : (reindex e e) B = B') (b : ↑B'.normTwoShell) : ↑((normTwoShellCongr he).symm b) = ↑b ∘ ⇑e

theorem Matrix.dotProduct_mulVec_pow_normTwoShellCongr {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (σ : Equiv.Perm I) (hσ : (reindex σ σ) B = B) (h : I → ℤ) (hh : h ∘ ⇑(Equiv.symm σ) = h) (a : ↑B.normTwoShell) (r : ℕ) : h ⬝ᵥ B.mulVec ↑((normTwoShellCongr hσ ^ r) a) = h ⬝ᵥ B.mulVec ↑a

Pairing with an invariant lattice vector is constant along a root orbit.

theorem Matrix.apply_mem_normTwoShell_iff {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {a : I → ℤ} {J : Type u_2} [Fintype J] {B' : Matrix J J ℤ} {g : (I → ℤ) → J → ℤ} (hg : ∀ (a b : I → ℤ), g a ⬝ᵥ B'.mulVec (g b) = a ⬝ᵥ B.mulVec b) : g a ∈ B'.normTwoShell ↔ a ∈ B.normTwoShell

A vector lies in the norm-two shell of B exactly when its image under an isometry from the Gram lattice of B to that of B' lies in the norm-two shell of B'.

def Matrix.normTwoShellEquivOfIsometry {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {J : Type u_2} [Fintype J] {B' : Matrix J J ℤ} (g : (I → ℤ) ≃ₗ[ℤ] J → ℤ) (hg : ∀ (a b : I → ℤ), g a ⬝ᵥ B'.mulVec (g b) = a ⬝ᵥ B.mulVec b) : ↑B.normTwoShell ≃ ↑B'.normTwoShell

The norm-two shells of isometric Gram lattices: a linear isometry g from the Gram lattice of B onto that of B' restricts to a bijection a ↦ g a from the norm-two shell of B to that of B'.

@[simp]

theorem Matrix.coe_normTwoShellEquivOfIsometry_apply {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {J : Type u_2} [Fintype J] {B' : Matrix J J ℤ} (g : (I → ℤ) ≃ₗ[ℤ] J → ℤ) (hg : ∀ (a b : I → ℤ), g a ⬝ᵥ B'.mulVec (g b) = a ⬝ᵥ B.mulVec b) (a : ↑B.normTwoShell) : ↑((normTwoShellEquivOfIsometry g hg) a) = g ↑a

@[simp]

theorem Matrix.coe_normTwoShellEquivOfIsometry_symm_apply {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {J : Type u_2} [Fintype J] {B' : Matrix J J ℤ} (g : (I → ℤ) ≃ₗ[ℤ] J → ℤ) (hg : ∀ (a b : I → ℤ), g a ⬝ᵥ B'.mulVec (g b) = a ⬝ᵥ B.mulVec b) (b : ↑B'.normTwoShell) : ↑((normTwoShellEquivOfIsometry g hg).symm b) = g.symm ↑b

theorem Matrix.normTwoShellEquivOfIsometry_funCongrLeft {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} {J : Type u_2} [Fintype J] {B' : Matrix J J ℤ} {e : I ≃ J} (he : (reindex e e) B = B') (hg : ∀ (a b : I → ℤ), (LinearEquiv.funCongrLeft ℤ ℤ e.symm) a ⬝ᵥ B'.mulVec ((LinearEquiv.funCongrLeft ℤ ℤ e.symm) b) = a ⬝ᵥ B.mulVec b) (a : ↑B.normTwoShell) : (normTwoShellEquivOfIsometry (LinearEquiv.funCongrLeft ℤ ℤ e.symm) hg) a = (normTwoShellCongr he) a

The isometry a ↦ a ∘ e.symm induced by a relabelling e restricts on the norm-two shells to the relabelling bijection Matrix.normTwoShellCongr.