Type-Aₙ root systems

Explicit construction of the type-Aₙ root pairing on the weight lattice Fin n → ℤ, exhibited as a crystallographic, reduced Mathlib RootPairing.

@[reducible, inline]

abbrev An.Zn (n : ℕ) : Type

The integral weight lattice Fin n → ℤ underlying the type-Aₙ root pairing.

Equations

• An.Zn n = (Fin n → ℤ)

@[reducible, inline]

abbrev An.ZnDual (n : ℕ) : Type

The ℤ-linear dual of Zn n, carrying the coroots.

Equations

• An.ZnDual n = Module.Dual ℤ (An.Zn n)

def An.eTranspose {n : ℕ} (k : Fin n) : ZnDual n

The covector extracting the k-th coordinate of a vector in Zn n.

Equations

• An.eTranspose k = { toFun := fun (t : An.Zn n) => t k, map_add' := ⋯, map_smul' := ⋯ }

def An.Ae {n : ℕ} (k : Fin n) : Zn n

The k-th column vector: 2 at index k, -1 at the neighbours of k, and 0 elsewhere.

Equations

• An.Ae k t = if t = k then 2 else if ↑k + 1 = ↑t ∨ ↑t + 1 = ↑k then -1 else 0

structure An.SignedInterval (n : ℕ) : Type

A signed interval [i, j] in Fin n with a sign ε; indexes the roots of type Aₙ.

• i : Fin n

  The left endpoint of the interval.

• j : Fin n

  The right endpoint of the interval.

• hij : self.i ≤ self.j
• ε : Bool

  The Boolean sign attached to the interval.

def An.SignedInterval.sign {n : ℕ} (J : SignedInterval n) : ℤ

The integer sign of a signed interval: 1 when ε is true, otherwise -1.

Equations

• J.sign = if J.ε = true then 1 else -1

def An.α {n : ℕ} (J : SignedInterval n) : Zn n

The root of type Aₙ associated to a signed interval.

Equations

• An.α J = J.sign • ∑ k ∈ Finset.Icc J.i J.j, An.Ae k

def An.αDual {n : ℕ} (J : SignedInterval n) : ZnDual n

The coroot of type Aₙ associated to a signed interval.

Equations

• An.αDual J = J.sign • ∑ k ∈ Finset.Icc J.i J.j, An.eTranspose k

def An.s {n : ℕ} (J K : SignedInterval n) : SignedInterval n

The reflection permutation for signed intervals. For positive intervals J = [i,j] and K = [k,l]:

• If (i,j) = (k,l): returns -[k,l]
• If i = l+1: returns [k,j] (merge: K then J)
• If k = j+1: returns [i,l] (merge: J then K)
• If i = k, j > l: returns -[l+1, j]
• If i = k, j < l: returns [j+1, l]
• If i < k, j = l: returns -[i, k-1]
• If i > k, j = l: returns [k, i-1]
• Otherwise: returns [k,l] Then s_{-J} = s_J and s_J(-K) = -s_J(K).

Equations

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

@[reducible, inline]

noncomputable abbrev An.ZnPairing (n : ℕ) : Zn n →ₗ[ℤ] ZnDual n →ₗ[ℤ] ℤ

The canonical evaluation pairing between Zn n and its dual ZnDual n.

Equations

• An.ZnPairing n = Module.Dual.eval ℤ (An.Zn n)

theorem An.SignedInterval.ext' {n : ℕ} {J K : SignedInterval n} (hi : J.i = K.i) (hj : J.j = K.j) (hε : J.ε = K.ε) : J = K

theorem An.SignedInterval.ext'_iff {n : ℕ} {J K : SignedInterval n} : J = K ↔ J.i = K.i ∧ J.j = K.j ∧ J.ε = K.ε

theorem An.s_involutive {n : ℕ} [NeZero n] (J K : SignedInterval n) : s J (s J K) = K

theorem An.Ae_sum_eq {n : ℕ} [NeZero n] (p q : Fin n) (hpq : p ≤ q) (t : Fin n) : (∑ u ∈ Finset.Icc p q, Ae u) t = (((if t = p then 1 else 0) + if t = q then 1 else 0) - if ↑t + 1 = ↑p then 1 else 0) - if ↑q + 1 = ↑t then 1 else 0

The key formula: sum of Ae columns over an interval [p,q] evaluated at t gives δ_{t,p} + δ_{t,q} - δ_{t+1,p} - δ_{q+1,t} (using ℕ comparisons).

theorem An.α_eval {n : ℕ} [NeZero n] (J : SignedInterval n) (t : Fin n) : α J t = J.sign * ((((if t = J.i then 1 else 0) + if t = J.j then 1 else 0) - if ↑t + 1 = ↑J.i then 1 else 0) - if ↑J.j + 1 = ↑t then 1 else 0)

α J evaluated at t, expressed in terms of Kronecker deltas.

theorem An.α_dual_eval {n : ℕ} [NeZero n] (J : SignedInterval n) (f : Zn n) : (αDual J) f = J.sign * ∑ v ∈ Finset.Icc J.i J.j, f v

αDual J evaluated on a test function.

theorem An.pairing_formula {n : ℕ} [NeZero n] (J K : SignedInterval n) : ((ZnPairing n) (α K)) (αDual J) = J.sign * K.sign * ((((if J.i = K.i then 1 else 0) + if J.j = K.j then 1 else 0) - if ↑J.i = ↑K.j + 1 then 1 else 0) - if ↑K.i = ↑J.j + 1 then 1 else 0)

Pairing computation: L(α K, α^v J) in terms of interval endpoints.

theorem An.pairing_self {n : ℕ} [NeZero n] (J : SignedInterval n) : ((ZnPairing n) (α J)) (αDual J) = 2

theorem An.pairing_eq_two_iff_eq {n : ℕ} [NeZero n] (J K : SignedInterval n) : ((ZnPairing n) (α K)) (αDual J) = 2 ↔ K = J

theorem An.α_injective {n : ℕ} [NeZero n] : Function.Injective α

theorem An.α_dual_injective {n : ℕ} [NeZero n] : Function.Injective αDual

theorem An.root_coroot_two' {n : ℕ} [NeZero n] (J : SignedInterval n) : ((ZnPairing n) (α J)) (αDual J) = 2

theorem An.reflectionPerm_root_eval {n : ℕ} [NeZero n] (J K : SignedInterval n) (t : Fin n) : (α K - ((ZnPairing n) (α K)) (αDual J) • α J) t = α (s J K) t

theorem An.reflectionPerm_root' {n : ℕ} [NeZero n] (J K : SignedInterval n) : α K - ((ZnPairing n) (α K)) (αDual J) • α J = α (s J K)

theorem An.pairing_symm {n : ℕ} [NeZero n] (J K : SignedInterval n) : ((ZnPairing n) (α J)) (αDual K) = ((ZnPairing n) (α K)) (αDual J)

theorem An.reflectionPerm_coroot_single {n : ℕ} [NeZero n] (J K : SignedInterval n) (t : Fin n) : ((αDual K - ((ZnPairing n) (α J)) (αDual K) • αDual J) ∘ₗ LinearMap.single ℤ (fun (x : Fin n) => ℤ) t) 1 = (αDual (s J K) ∘ₗ LinearMap.single ℤ (fun (x : Fin n) => ℤ) t) 1

theorem An.reflectionPerm_coroot' {n : ℕ} [NeZero n] (J K : SignedInterval n) : αDual K - ((ZnPairing n) (α J)) (αDual K) • αDual J = αDual (s J K)

noncomputable def An.rootPairing (n : ℕ) [NeZero n] : RootPairing (SignedInterval n) ℤ (Zn n) (ZnDual n)

The type-Aₙ root pairing over ℤ, built from signed intervals on Fin n.

Equations

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

@[implicit_reducible]

instance An.finite (n : ℕ) : Fintype (SignedInterval n)

Equations

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

theorem An.An_is_finite (n : ℕ) [NeZero n] : Finite (SignedInterval n)

theorem An.An_is_reduced (n : ℕ) [NeZero n] : (rootPairing n).IsReduced

theorem An.An_is_crystallographic (n : ℕ) [NeZero n] : (rootPairing n).IsCrystallographic