The shifted weights of the orthogonal groups

The Weyl dimension formulas for SO (2n + 1) (type Bₙ) and SO (2n) (type Dₙ) both read a Young diagram μ through the integers xᵢ = μᵢ + n - 1 - i. For type Dₙ the half-sum of the positive roots is ρ = (n - 1, …, 0), and the xᵢ are the entries of μ + ρ; for type Bₙ it is ρ = (n - 1/2, …, 1/2), and the xᵢ are the entries of μ + ρ less 1/2. This file records the sequence and the two properties of it that make the factors of both numerators positive.

Main definitions

• TauCeti.orthogonalRhoShift: the integers μᵢ + n - 1 - i.

def TauCeti.orthogonalRhoShift (n : ℕ) (μ : YoungDiagram) (i : ℕ) : ℤ

The integers μᵢ + n - 1 - i, shared by the orthogonal groups: the entries of μ + ρ for the half-sum ρ = (n - 1, …, 0) of the positive roots of type Dₙ (SO (2n)), and the entries μᵢ + n - i - 1/2 of μ + ρ less 1/2 for the half-sum ρ = (n - 1/2, …, 1/2) of the positive roots of type Bₙ (SO (2n + 1)). Only the indices i < n are used.

@[simp]

theorem TauCeti.orthogonalRhoShift_apply (n : ℕ) (μ : YoungDiagram) (i : ℕ) : orthogonalRhoShift n μ i = ↑(μ.rowLen i) + ↑n - 1 - ↑i

The defining equation of TauCeti.orthogonalRhoShift.

theorem TauCeti.orthogonalRhoShift_nonneg {n : ℕ} {μ : YoungDiagram} {i : ℕ} (hi : i < n) : 0 ≤ orthogonalRhoShift n μ i

The shifted entries are nonnegative below n.

theorem TauCeti.orthogonalRhoShift_strictAnti (n : ℕ) (μ : YoungDiagram) : StrictAnti (orthogonalRhoShift n μ)

Adding the strictly decreasing ρ to the weakly decreasing row lengths gives a strictly decreasing sequence, which makes every factor of the orthogonal Weyl dimension numerators positive.