The root operators on piecewise-linear paths are partial inverses

Fix a vector x : V and a linear form f : V → 𝕜 with f x = 2; in Littelmann's path model x is a simple root α and f the pairing with its coroot. This file proves that Littelmann's lowering and raising operators f_α = TauCeti.PLPath.lower f x and e_α = TauCeti.PLPath.raise f x are partial inverses on all piecewise-linear paths: f_α π = π' exactly when e_α π' = π. This is the partial-inverse axiom of a crystal; no integrality of the path is needed.

Capped reflection TauCeti.PLPath.reflectRecords f x c reflects the pieces of a path along which the running height H is at most c and at most every later height: it subtracts (min c (m t) - min c h) • x at time t, where m t is the minimum of H on [t, 1] and h the minimal height. Lowering is the case c = h + 1. Since e_α is f_α conjugated by reversal, the key identity is that the inverse of this capped reflection is again a capped reflection, on the reversed lowered path, whose cap is h minus the final height of the lowered path (TauCeti.PLPath.normalize_reflectRecords_reverse_map_neg_reflectRecords).

Main results

• TauCeti.PLPath.normalize_reflectRecords_reverse_map_neg_reflectRecords: capped reflection of a reversed path undoes capped reflection.
• TauCeti.PLPath.lower_eq_some_iff, TauCeti.PLPath.raise_eq_some_iff: f_α π = π' exactly when e_α π' = π.

References

• P. Littelmann, Paths and root operators in representation theory, Ann. of Math. 142 (1995), §1.

Undoing capped reflection

theorem TauCeti.PLPath.normalize_reflectRecords_reverse_map_neg_reflectRecords {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (hx : f x = 2) (c : 𝕜) (l : List V) : normalize 𝕜 (reflectRecords f x (listMinHeight f l - f (reflectRecords f x c l).sum) (List.map Neg.neg (reflectRecords f x c l)).reverse) = normalize 𝕜 (List.map Neg.neg l).reverse

Reflecting the records of a reversed path undoes the reflection of the records up to any cap c: if l' is obtained from l by reflecting its records up to c, then reflecting the records of the reversal of l' up to the minimal height of l minus the final height of l' gives back the reversal of l, up to the elementary moves.

The root operators are partial inverses

theorem TauCeti.PLPath.lower_eq_some_iff {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (hx : f x = 2) {p q : PLPath 𝕜 V} : lower f x p = some q ↔ raise f x q = some p

Littelmann's root operators are partial inverses: lowering p gives q exactly when raising q gives p.

theorem TauCeti.PLPath.raise_eq_some_iff {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (hx : f x = 2) {p q : PLPath 𝕜 V} : raise f x p = some q ↔ lower f x q = some p

Littelmann's root operators are partial inverses: raising p gives q exactly when lowering q gives p.