String lengths of the root operators on piecewise-linear paths

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. Write H(t) = f (π t) for the running height of a path π and h = min H for its minimal height (TauCeti.PLPath.minHeight). The single-step formulas in TauCeti.RepresentationTheory.LSPath.RootOperator show that the root operators f_α = TauCeti.PLPath.lower f x and e_α = TauCeti.PLPath.raise f x move the minimal height by exactly one step: min H(f_α π) = h - 1 and min H(e_α π) = h + 1. Since f_α lowers the final height by f x = 2, it shortens H(1) - h by one.

Together with the criteria f_α π = 0 ↔ H(1) - h < 1 and e_α π = 0 ↔ -1 < h, this computes the lengths of the root strings through every path: f_α ^ n π is defined exactly when n ≤ H(1) - h, and e_α ^ n π exactly when n ≤ -h. These ambient statements hold for every path. When h and H(1) are integers, as on Littelmann's integral paths, they become the string-length identities ε_α(π) = -h and φ_α(π) = H(1) - h of a normal crystal (TauCeti.NormalCrystal).

The key computation is the minimal height of capped reflection (TauCeti.PLPath.listMinHeight_reflectRecords): reflecting the pieces of a path along which the height is at most c and at most every later height lowers the minimal height by the increase min (H 1) c - min h c, just as it lowers the final height by twice that amount.

Main results

• TauCeti.PLPath.lowerIter, TauCeti.PLPath.raiseIter: iterated partial root operators, with composition, reversal, endpoint and minimum-height formulas.
• TauCeti.PLPath.isSome_lowerIter_iff, TauCeti.PLPath.isSome_raiseIter_iff: the lengths of the root strings through a path.
• TauCeti.PLPath.isSome_lowerIter_iff_of_eq_natCast, TauCeti.PLPath.isSome_raiseIter_iff_of_eq_natCast: the string-length identities φ_α = H(1) - h and ε_α = -h when these are natural numbers.

References

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

Iterated root operators

noncomputable def TauCeti.PLPath.lowerIter {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (f : Module.Dual 𝕜 V) (x : V) : ℕ → PLPath 𝕜 V → Option (PLPath 𝕜 V)

Apply lowering n times, returning none as soon as an application is undefined.

noncomputable def TauCeti.PLPath.raiseIter {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (f : Module.Dual 𝕜 V) (x : V) : ℕ → PLPath 𝕜 V → Option (PLPath 𝕜 V)

Apply raising n times, returning none as soon as an application is undefined.

@[simp]

theorem TauCeti.PLPath.lowerIter_zero {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (p : PLPath 𝕜 V) : lowerIter f x 0 p = some p

@[simp]

theorem TauCeti.PLPath.raiseIter_zero {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (p : PLPath 𝕜 V) : raiseIter f x 0 p = some p

theorem TauCeti.PLPath.lowerIter_succ {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (n : ℕ) (p : PLPath 𝕜 V) : lowerIter f x (n + 1) p = (lower f x p).bind (lowerIter f x n)

theorem TauCeti.PLPath.raiseIter_succ {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (n : ℕ) (p : PLPath 𝕜 V) : raiseIter f x (n + 1) p = (raise f x p).bind (raiseIter f x n)

@[simp]

theorem TauCeti.PLPath.lowerIter_one {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (p : PLPath 𝕜 V) : lowerIter f x 1 p = lower f x p

@[simp]

theorem TauCeti.PLPath.raiseIter_one {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (p : PLPath 𝕜 V) : raiseIter f x 1 p = raise f x p

theorem TauCeti.PLPath.raiseIter_eq_map_lowerIter_reverse {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (n : ℕ) (p : PLPath 𝕜 V) : raiseIter f x n p = Option.map reverse (lowerIter f x n p.reverse)

Iterated raising is iterated lowering conjugated by reversal.

theorem TauCeti.PLPath.lowerIter_add {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (m n : ℕ) (p : PLPath 𝕜 V) : lowerIter f x (m + n) p = (lowerIter f x m p).bind (lowerIter f x n)

Concatenating two runs of the lowering operator.

theorem TauCeti.PLPath.raiseIter_add {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (m n : ℕ) (p : PLPath 𝕜 V) : raiseIter f x (m + n) p = (raiseIter f x m p).bind (raiseIter f x n)

Concatenating two runs of the raising operator.

theorem TauCeti.PLPath.endpoint_of_lowerIter_eq_some {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p q : PLPath 𝕜 V} {n : ℕ} (h : lowerIter f x n p = some q) : q.endpoint = p.endpoint - n • x

Lowering n times subtracts n copies of the root from the endpoint.

theorem TauCeti.PLPath.minHeight_of_lowerIter_eq_some {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p q : PLPath 𝕜 V} {n : ℕ} (hx : f x = 2) (h : lowerIter f x n p = some q) : minHeight f q = minHeight f p - ↑n

Lowering n times decreases the minimum height by n.

theorem TauCeti.PLPath.endpoint_of_raiseIter_eq_some {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p q : PLPath 𝕜 V} {n : ℕ} (h : raiseIter f x n p = some q) : q.endpoint = p.endpoint + n • x

Raising n times adds n copies of the root to the endpoint.

theorem TauCeti.PLPath.minHeight_of_raiseIter_eq_some {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p q : PLPath 𝕜 V} {n : ℕ} (hx : f x = 2) (h : raiseIter f x n p = some q) : minHeight f q = minHeight f p + ↑n

Raising n times increases the minimum height by n.

Lengths of the root strings

@[simp]

theorem TauCeti.PLPath.isSome_lowerIter_iff {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p : PLPath 𝕜 V} {n : ℕ} (hx : f x = 2) : (lowerIter f x n p).isSome = true ↔ ↑n ≤ f p.endpoint - minHeight f p

The exact bound for iterated lowering. No integrality hypothesis on the path is needed.

@[simp]

theorem TauCeti.PLPath.isSome_raiseIter_iff {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p : PLPath 𝕜 V} {n : ℕ} (hx : f x = 2) : (raiseIter f x n p).isSome = true ↔ ↑n ≤ -minHeight f p

The exact bound for iterated raising. Integral negative minimum height is therefore the usual raising-string length.

@[simp]

theorem TauCeti.PLPath.lowerIter_eq_none_iff {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p : PLPath 𝕜 V} {n : ℕ} (hx : f x = 2) : lowerIter f x n p = none ↔ f p.endpoint - minHeight f p < ↑n

Iterated lowering is undefined precisely beyond its height bound.

@[simp]

theorem TauCeti.PLPath.raiseIter_eq_none_iff {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p : PLPath 𝕜 V} {n : ℕ} (hx : f x = 2) : raiseIter f x n p = none ↔ -minHeight f p < ↑n

Iterated raising is undefined precisely beyond its height bound.

theorem TauCeti.PLPath.isSome_lowerIter_iff_of_eq_natCast {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p : PLPath 𝕜 V} (hx : f x = 2) {φ : ℕ} (hφ : f p.endpoint - minHeight f p = ↑φ) (n : ℕ) : (lowerIter f x n p).isSome = true ↔ n ≤ φ

The string-length identity φ_α = H(1) - min H: when H(1) - min H is a natural number φ, the lowering string through the path has length exactly φ.

theorem TauCeti.PLPath.isSome_raiseIter_iff_of_eq_natCast {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {p : PLPath 𝕜 V} (hx : f x = 2) {ε : ℕ} (hε : -minHeight f p = ↑ε) (n : ℕ) : (raiseIter f x n p).isSome = true ↔ n ≤ ε

The string-length identity ε_α = -min H: when -min H is a natural number ε, the raising string through the path has length exactly ε.