Type-BCₙ root systems

Explicit construction of the type-BCₙ root pairing from the standard dot product on ℤⁿ, exhibited as a Mathlib RootPairing, together with a characterization of its roots as the classical type-BCₙ root set {±eᵢ, ±2eᵢ, ±eᵢ ± eⱼ (i ≠ j)} (BCn.isReflective_iff_isClassicalRoot, BCn.range_rootPairing_root).

@[reducible, inline]

abbrev BCn.Space (n : ℕ) : Type

The ambient space Fin n → ℤ for the type-BCₙ construction.

Equations

• BCn.Space n = (Fin n → ℤ)

@[reducible, inline]

abbrev BCn.CoSpace (n : ℕ) : Type

The ℤ-linear dual of Space n.

Equations

• BCn.CoSpace n = Module.Dual ℤ (BCn.Space n)

noncomputable def BCn.dotProduct (n : ℕ) : Space n →ₗ[ℤ] Space n →ₗ[ℤ] ℤ

The standard dot product on ℤⁿ.

Equations

• BCn.dotProduct n = { toFun := fun (x : BCn.Space n) => { toFun := fun (y : BCn.Space n) => ∑ i : Fin n, x i * y i, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

theorem BCn.dotProduct_apply (n : ℕ) (x y : Space n) : ((dotProduct n) x) y = ∑ i : Fin n, x i * y i

@[simp]

theorem BCn.dotProduct_single_right {n : ℕ} (x : Space n) (i : Fin n) : ((dotProduct n) x) (Pi.single i 1) = x i

@[simp]

theorem BCn.dotProduct_single_left {n : ℕ} (x : Space n) (i : Fin n) : ((dotProduct n) (Pi.single i 1)) x = x i

theorem BCn.dotProduct_isSymm (n : ℕ) : (dotProduct n).IsSymm

theorem BCn.dotProduct_nondegenerate (n : ℕ) : (dotProduct n).Nondegenerate

@[reducible, inline]

abbrev BCn.ReflectiveIndex (n : ℕ) : Type

The reflective vectors for the standard dot product.

Equations

• BCn.ReflectiveIndex n = { x : BCn.Space n // (BCn.dotProduct n).IsReflective x }

noncomputable def BCn.rootPairing (n : ℕ) : RootPairing (ReflectiveIndex n) ℤ (Space n) (CoSpace n)

The BCₙ root pairing, built from all reflective vectors for the standard dot product.

Equations

• BCn.rootPairing n = RootPairing.ofBilinear (BCn.dotProduct n) ⋯ ⋯ BCn.rootPairing._proof_3

Characterization of the type-BCₙ roots

The reflective vectors of the standard dot product on ℤⁿ are exactly the classical type-BCₙ roots ±eᵢ, ±2eᵢ, and ±eᵢ ± eⱼ for i ≠ j.

theorem BCn.dotProduct_single_left_eq {n : ℕ} (i : Fin n) (a : ℤ) (y : Space n) : ((dotProduct n) (Pi.single i a)) y = a * y i

def BCn.IsClassicalRoot {n : ℕ} (x : Space n) : Prop

The classical type-BCₙ root set: x is a classical root when it is ±eᵢ or ±2eᵢ for some i, or ±eᵢ ± eⱼ for some i ≠ j, where eᵢ is the i-th standard basis vector of ℤⁿ.

Equations

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

theorem BCn.eq_single_of_eq_zero {n : ℕ} {x : Space n} {i : Fin n} (h : ∀ (k : Fin n), k ≠ i → x k = 0) : x = Pi.single i (x i)

theorem BCn.eq_single_add_single_of_eq_zero {n : ℕ} {x : Space n} {i j : Fin n} (hij : i ≠ j) (h : ∀ (k : Fin n), k ≠ i → k ≠ j → x k = 0) : x = Pi.single i (x i) + Pi.single j (x j)

theorem BCn.isClassicalRoot_of_isReflective {n : ℕ} {x : Space n} (hx : (dotProduct n).IsReflective x) : IsClassicalRoot x

theorem BCn.isReflective_of_isClassicalRoot {n : ℕ} {x : Space n} (hx : IsClassicalRoot x) : (dotProduct n).IsReflective x

theorem BCn.isReflective_iff_isClassicalRoot {n : ℕ} (x : Space n) : (dotProduct n).IsReflective x ↔ IsClassicalRoot x

A vector of ℤⁿ is reflective for the standard dot product precisely when it is one of the classical type-BCₙ roots ±eᵢ, ±2eᵢ, or ±eᵢ ± eⱼ with i ≠ j.

theorem BCn.range_rootPairing_root (n : ℕ) : Set.range ⇑(rootPairing n).root = {x : Space n | IsClassicalRoot x}

The roots of the type-BCₙ root pairing are exactly the classical type-BCₙ roots ±eᵢ, ±2eᵢ, and ±eᵢ ± eⱼ for i ≠ j.