The normalisation of an invariant form against the coroots

Mathlib's RootPairing.InvariantForm.two_mul_apply_root_root computes an invariant form on two roots through the Cartan integers: 2 ⟨αᵢ, αⱼ⟩ = ⟨αᵢ, αⱼ^∨⟩ ⟨αⱼ, αⱼ⟩. Nothing in that argument uses that the first argument is a root, and this file records the identity for an arbitrary vector of the weight space:

2 ⟨x, α⟩ = ⟨x, α^∨⟩ ⟨α, α⟩,

that is, the coroot α^∨ is 2α / ⟨α, α⟩ under the identification of weights and coweights that the form provides. It converts any expression in the pairings ⟨x, α⟩ of an invariant form into one in the coroot values ⟨x, α^∨⟩, which is how the Weyl dimension formula passes from the form in which it is proved to its division-free integer statement.

Main results

• RootPairing.InvariantForm.two_mul_apply_root: 2 ⟨x, α⟩ = ⟨x, α^∨⟩ ⟨α, α⟩ for every x.

theorem RootPairing.InvariantForm.two_mul_apply_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : P.InvariantForm) (x : M) (j : ι) : 2 * (B.form x) (P.root j) = (P.coroot' j) x * (B.form (P.root j)) (P.root j)

The normalisation of an invariant form against a coroot: 2 ⟨x, α⟩ = ⟨x, α^∨⟩ ⟨α, α⟩ for every vector x of the weight space. This extends RootPairing.InvariantForm.two_mul_apply_root_root from the roots to all of M.