Reflection-invariant submodules of a root pairing

A submodule of the root space invariant under the reflection at v absorbs, from any root it already contains, every root whose pairing with v is nonzero. Reflecting u in v stays inside the submodule, and subtracting leaves a multiple of the root at v whose coefficient is exactly that pairing.

This is stated for a bare RootPairing: no base, no crystallographic structure, no finiteness and no assumption on the characteristic. Consumers that propagate membership along a Dynkin edge supply the nonvanishing of the pairing from adjacency at the call site.

Main results

• RootPairing.root_mem_of_pairing_ne_zero: membership of a root in a reflection-invariant submodule propagates along a nonzero pairing.

theorem RootPairing.root_mem_of_pairing_ne_zero {K : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootPairing ι K M N} {q : Submodule K M} {u v : ι} (hinvv : q ∈ Module.End.invtSubmodule ↑(P.reflection v)) (hpair : P.pairing u v ≠ 0) (hu : P.root u ∈ q) : P.root v ∈ q

Membership of a root in a reflection-invariant submodule propagates along a nonzero pairing. If q is invariant under the reflection at v, the pairing of u with v is nonzero, and the root at u lies in q, then so does the root at v.