Running heights and root operators on piecewise-linear paths

Fix a vector x : V and a linear form f : V → 𝕜; in Littelmann's path model x is a simple root α and f the pairing ⟨-, α^∨⟩ with its coroot, so that f x = 2 and Module.preReflection x f is the simple reflection s_α. The running height of a path π is t ↦ f (π t). For a path presented by a segment list [v₁, …, vₙ] the height is affine on each segment, so its minimum h is attained at a vertex, that is at a partial sum v₁ + ⋯ + vₖ; TauCeti.PLPath.minHeight is this minimum. It is independent of the presentation. On Littelmann's path crystals the string lengths are ε = -h and φ = f (π 1) - h.

Littelmann's lowering operator f_α is defined when f (π 1) - h ≥ 1. Let t₀ be the last time at which the height equals h, and t₁ the first time from which on the height is at least h + 1. Subdivide the piece of π from t₀ to t₁ into pieces of two kinds: those along which the height increases and stays at most every later height, and equal-height excursions, along which the height starts and ends at the same value and stays at least that value. Then f_α π reflects the pieces of the first kind by s_α, keeps the excursions, and translates the rest of π after t₁ by -α. Equivalently, with m t the minimum of the height on [t, 1], f_α π t = π t - min 1 (m t - h) • α. In terms of segments, each segment is cut at most once, and its reflected part is the initial piece along which the height stays at most both h + 1 and every later height. The raising operator e_α is conjugate to f_α by the reversal π ↦ π^∨ of paths; it is defined when h ≤ -1. With t₁ the first time at which the height equals h and t₀ the last time up to which the height is at least h + 1, it reflects the pieces between t₀ and t₁ along which the height decreases and stays at most every earlier height, keeps the equal-height excursions, and translates the rest of π after t₁ by α.

The operators are defined on segment lists (TauCeti.PLPath.reflectRecords, TauCeti.PLPath.listLower) and then on TauCeti.PLPath, using its reduced presentation. The main result of this file is that the operators do not depend on the chosen presentation: the elementary moves (subdividing a segment, inserting a stationary segment) commute with them up to the same moves. The weight changes by -α under f_α and by α under e_α, while the minimal height changes by -1 and +1, respectively, when f x = 2.

This file works with the ambient operators on all paths. That e_α and f_α are partial inverses is proved in TauCeti.RepresentationTheory.LSPath.PartialInverse, and the lengths of the root strings through a path in TauCeti.RepresentationTheory.LSPath.StringLength.

Main definitions

• TauCeti.PLPath.minHeight: the minimum of the running height t ↦ f (π t).
• TauCeti.PLPath.lower, TauCeti.PLPath.raise: Littelmann's root operators f_α and e_α, with none standing for 0.

Main results

• TauCeti.PLPath.exists_listMinHeight_eq, TauCeti.PLPath.listMinHeight_le_apply_sum_take: the minimal height of a presentation is the minimum of the heights of its vertices.
• TauCeti.PLPath.minHeight_ofSegments, TauCeti.PLPath.minHeight_mul, TauCeti.PLPath.minHeight_reverse: the minimal height is independent of the presentation, and its behaviour under concatenation and reversal.
• TauCeti.PLPath.reflectRecords_append: capped reflection TauCeti.PLPath.reflectRecords of a concatenation.
• TauCeti.PLPath.reflectRecords_of_le_listMinHeight: capped reflection is the identity when the cap is at most the minimal height.
• TauCeti.PLPath.ofSegments_reflectRecords_of_forall_nonneg: capped reflection, up to the final height, of a path whose segments all have nonnegative height reflects the whole path.
• TauCeti.PLPath.lower_ofSegments: the lowering operator may be computed on any presentation.
• TauCeti.PLPath.lower_eq_none_iff, TauCeti.PLPath.raise_eq_none_iff: f_α π = 0 exactly when f (π 1) - h < 1, and e_α π = 0 exactly when -1 < h.
• TauCeti.PLPath.endpoint_of_lower_eq_some, TauCeti.PLPath.endpoint_of_raise_eq_some: the root operators change the endpoint by ∓ α.
• TauCeti.PLPath.listMinHeight_reflectRecords: the minimal height of capped reflection.
• TauCeti.PLPath.minHeight_of_lower_eq_some, TauCeti.PLPath.minHeight_of_raise_eq_some: f_α lowers and e_α raises the minimal height by one.
• TauCeti.PLPath.lower_straight: lowering a straight path t ↦ t • v with f v ≥ 1.

References

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

The minimal height of a segment list

def TauCeti.PLPath.listMinHeight {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] (f : Module.Dual 𝕜 V) : List V → 𝕜

The running-height recursion for a segment list. When addition preserves the scalar order, this is the minimum of f over the vertices 0, v₁, v₁ + v₂, …, v₁ + ⋯ + vₙ. For a piecewise-linear path over an ordered field, the minimum of its affine height on each segment is attained at a vertex.

@[simp]

theorem TauCeti.PLPath.listMinHeight_nil {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} : listMinHeight f [] = 0

@[simp]

theorem TauCeti.PLPath.listMinHeight_cons {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (v : V) (l : List V) : listMinHeight f (v :: l) = min 0 (f v + listMinHeight f l)

@[simp]

theorem TauCeti.PLPath.listMinHeight_map {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {W : Type u_3} [AddCommMonoid W] [Module 𝕜 W] (g : V →ₗ[𝕜] W) (f' : Module.Dual 𝕜 W) (l : List V) : listMinHeight f' (List.map (⇑g) l) = listMinHeight (f' ∘ₗ g) l

The vertex heights of a linear image are computed by the pulled-back form.

theorem TauCeti.PLPath.listMinHeight_map_smul {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} [PosMulMono 𝕜] {a : 𝕜} (ha : 0 ≤ a) (l : List V) : listMinHeight f (List.map (fun (x : V) => a • x) l) = a * listMinHeight f l

Nonnegative dilation multiplies every vertex height and its minimum by the same scalar.

theorem TauCeti.PLPath.listMinHeight_nonpos {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (l : List V) : listMinHeight f l ≤ 0

theorem TauCeti.PLPath.listMinHeight_eq_zero_of_forall_nonneg {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {l : List V} (h : ∀ v ∈ l, 0 ≤ f v) : listMinHeight f l = 0

A path whose segments all have nonnegative height never goes below its starting height.

theorem TauCeti.PLPath.exists_listMinHeight_eq {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (l : List V) : ∃ (n : ℕ), listMinHeight f l = f (List.take n l).sum

The minimal height is the height of some vertex.

theorem TauCeti.PLPath.listMinHeight_le_apply_sum_take {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} [IsOrderedAddMonoid 𝕜] (l : List V) (n : ℕ) : listMinHeight f l ≤ f (List.take n l).sum

The minimal height is at most the height of each vertex.

theorem TauCeti.PLPath.listMinHeight_le_apply_sum {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} [IsOrderedAddMonoid 𝕜] (l : List V) : listMinHeight f l ≤ f l.sum

@[simp]

theorem TauCeti.PLPath.listMinHeight_append {𝕜 : Type u_1} {V : Type u_2} [Semiring 𝕜] [LinearOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} [IsOrderedAddMonoid 𝕜] (l₁ l₂ : List V) : listMinHeight f (l₁ ++ l₂) = min (listMinHeight f l₁) (f l₁.sum + listMinHeight f l₂)

theorem TauCeti.PLPath.listMinHeight_reverse_map_neg {𝕜 : Type u_1} {V : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (l : List V) : listMinHeight f (List.map Neg.neg l).reverse = listMinHeight f l - f l.sum

Reversing and negating the segments shifts their minimal height by the negative final height.

The minimal height of a path

theorem TauCeti.PLPath.listMinHeight_consMerge {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (v : V) (l : List V) : listMinHeight f (consMerge 𝕜 v l) = listMinHeight f (v :: l)

@[simp]

theorem TauCeti.PLPath.listMinHeight_normalize {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (l : List V) : listMinHeight f (normalize 𝕜 l) = listMinHeight f l

theorem TauCeti.PLPath.Move.listMinHeight_eq {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {l₁ l₂ : List V} (h : Move 𝕜 l₁ l₂) : listMinHeight f l₁ = listMinHeight f l₂

The minimal height is invariant under the elementary moves.

def TauCeti.PLPath.minHeight {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (f : Module.Dual 𝕜 V) (p : PLPath 𝕜 V) : 𝕜

The minimal running height min_t f (π t) of a path.

theorem TauCeti.PLPath.minHeight_def {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (p : PLPath 𝕜 V) : minHeight f p = listMinHeight f p.segments

@[simp]

theorem TauCeti.PLPath.minHeight_ofSegments {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (l : List V) : minHeight f (ofSegments 𝕜 l) = listMinHeight f l

The minimal height of a path may be computed on any presentation.

@[simp]

theorem TauCeti.PLPath.minHeight_map {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] (p : PLPath 𝕜 V) (g : V →ₗ[𝕜] W) (f' : Module.Dual 𝕜 W) : minHeight f' (p.map g) = minHeight (f' ∘ₗ g) p

Minimum height is natural under arbitrary linear maps.

theorem TauCeti.PLPath.minHeight_map_smul {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {a : 𝕜} (ha : 0 ≤ a) (p : PLPath 𝕜 V) : minHeight f (p.map (a • LinearMap.id)) = a * minHeight f p

Nonnegative dilation scales the minimum running height.

@[simp]

theorem TauCeti.PLPath.minHeight_one {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} : minHeight f 1 = 0

theorem TauCeti.PLPath.minHeight_nonpos {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (p : PLPath 𝕜 V) : minHeight f p ≤ 0

theorem TauCeti.PLPath.minHeight_le_apply_endpoint {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (p : PLPath 𝕜 V) : minHeight f p ≤ f p.endpoint

@[simp]

theorem TauCeti.PLPath.minHeight_mul {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (p q : PLPath 𝕜 V) : minHeight f (p * q) = min (minHeight f p) (f p.endpoint + minHeight f q)

@[simp]

theorem TauCeti.PLPath.minHeight_reverse {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (p : PLPath 𝕜 V) : minHeight f p.reverse = minHeight f p - f p.endpoint

@[simp]

theorem TauCeti.PLPath.minHeight_straight {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} (v : V) : minHeight f (straight 𝕜 v) = min 0 (f v)

The lowering operator on segment lists

def TauCeti.PLPath.reflectRecords {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] (f : Module.Dual 𝕜 V) (x : V) (c : 𝕜) : List V → List V

reflectRecords f x c l reflects, by Module.preReflection x f, the pieces of the path presented by l along which the running height (starting from 0) increases, stays at most c, and is at most every later height; it keeps the rest of the path, in particular every excursion that returns to a height reached before. For a segment v followed by l, the height relative to the start of v is at least f v + listMinHeight f l from the end of v on. When r = min (f v + listMinHeight f l) c is positive, v is cut at height r into the reflected initial piece (r / f v) • v and the kept piece (1 - r / f v) • v.

def TauCeti.PLPath.listLower {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] (f : Module.Dual 𝕜 V) (x : V) (l : List V) : Option (List V)

Littelmann's lowering operator on segment lists. With h = listMinHeight f l, it is defined when the final height is at least h + 1, and then reflects the pieces of the path along which the height increases from h to h + 1 while staying at most every later height (TauCeti.PLPath.reflectRecords).

@[simp]

theorem TauCeti.PLPath.reflectRecords_nil {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (c : 𝕜) : reflectRecords f x c [] = []

theorem TauCeti.PLPath.reflectRecords_cons_of_pos {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x v : V} {l : List V} {c : 𝕜} (h : 0 < min (f v + listMinHeight f l) c) : reflectRecords f x c (v :: l) = (Module.preReflection x f) ((min (f v + listMinHeight f l) c / f v) • v) :: (1 - min (f v + listMinHeight f l) c / f v) • v :: reflectRecords f x (c - f v) l

theorem TauCeti.PLPath.reflectRecords_cons_of_nonpos {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x v : V} {l : List V} {c : 𝕜} (h : min (f v + listMinHeight f l) c ≤ 0) : reflectRecords f x c (v :: l) = v :: reflectRecords f x (c - f v) l

theorem TauCeti.PLPath.listLower_def {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (l : List V) : listLower f x l = if 1 ≤ f l.sum - listMinHeight f l then some (reflectRecords f x (listMinHeight f l + 1) l) else none

theorem TauCeti.PLPath.mem_of_mem_reflectRecords {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l : List V} {c : 𝕜} {T : Set V} (hpos : ∀ (a : 𝕜), 0 < a → ∀ v ∈ T, a • v ∈ T) (hs : Set.MapsTo (⇑(Module.preReflection x f)) T T) (hl : ∀ v ∈ l, v ∈ T) {w : V} (hw : w ∈ reflectRecords f x c l) (hw0 : w ≠ 0) : w ∈ T

Capped reflection only cuts segments at fractions in [0, 1] and reflects some of the pieces by s = preReflection x f. So if a set T is stable under positive rescaling and under s, and contains every segment of l, then it contains every nonstationary segment of reflectRecords f x c l.

theorem TauCeti.PLPath.sum_reflectRecords {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (c : 𝕜) (l : List V) : (reflectRecords f x c l).sum = l.sum - (min (f l.sum) c - min (listMinHeight f l) c) • x

Reflecting the records up to height c subtracts from the endpoint x times the increase, along the path, of the minimum of c and the later minimal height.

theorem TauCeti.PLPath.listMinHeight_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) : listMinHeight f (reflectRecords f x c l) = listMinHeight f l - (min (f l.sum) c - min (listMinHeight f l) c)

Reflecting the records up to height c lowers the minimal height by the increase, along the path, of the minimum of c and the later minimal height. Compare TauCeti.PLPath.sum_reflectRecords, by which the final height drops by twice this amount.

@[simp]

theorem TauCeti.PLPath.listLower_eq_none_iff {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l : List V} : listLower f x l = none ↔ f l.sum - listMinHeight f l < 1

theorem TauCeti.PLPath.sum_of_listLower_eq_some {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l₁ l₂ : List V} (h : listLower f x l₁ = some l₂) : l₂.sum = l₁.sum - x

theorem TauCeti.PLPath.reflectRecords_append {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (c : 𝕜) (l₁ l₂ : List V) : reflectRecords f x c (l₁ ++ l₂) = reflectRecords f x (min c (f l₁.sum + listMinHeight f l₂)) l₁ ++ reflectRecords f x (c - f l₁.sum) l₂

Reflecting the records of a concatenation l₁ ++ l₂ up to the cap c: on l₁, the later heights in l₂ act as a further cap.

@[simp]

theorem TauCeti.PLPath.reflectRecords_of_le_listMinHeight {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l : List V} {c : 𝕜} (h : c ≤ listMinHeight f l) : reflectRecords f x c l = l

Reflecting the records up to a cap that is at most the minimal height does nothing.

theorem TauCeti.PLPath.ofSegments_reflectRecords_of_forall_nonneg {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l : List V} (h : ∀ v ∈ l, 0 ≤ f v) : ofSegments 𝕜 (reflectRecords f x (f l.sum) l) = ofSegments 𝕜 (List.map (⇑(Module.preReflection x f)) l)

Capped reflection of a path with nonnegative segment heights, up to its final height, reflects the whole path.

Independence of the presentation

theorem TauCeti.PLPath.reflectRecords_zero_cons {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (c : 𝕜) (l : List V) : reflectRecords f x c (0 :: l) = 0 :: reflectRecords f x c l

theorem TauCeti.PLPath.Move.normalize_reflectRecords {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l₁ l₂ : List V} (h : Move 𝕜 l₁ l₂) (c : 𝕜) : normalize 𝕜 (reflectRecords f x c l₁) = normalize 𝕜 (reflectRecords f x c l₂)

Reflecting the records commutes with the elementary moves, up to elementary moves.

theorem TauCeti.PLPath.Move.map_normalize_listLower {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l₁ l₂ : List V} (h : Move 𝕜 l₁ l₂) : Option.map (normalize 𝕜) (listLower f x l₁) = Option.map (normalize 𝕜) (listLower f x l₂)

Lowering commutes with the elementary moves, up to elementary moves.

theorem TauCeti.PLPath.map_normalize_listLower_eq {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} {l₁ l₂ : List V} (h : normalize 𝕜 l₁ = normalize 𝕜 l₂) : Option.map (normalize 𝕜) (listLower f x l₁) = Option.map (normalize 𝕜) (listLower f x l₂)

Lowering does not depend on the presentation: presentations of the same path have lowerings presenting the same path.

Root operators on paths

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

Littelmann's lowering operator f_α on paths, for the root α = x and the coroot pairing f = ⟨-, α^∨⟩. Let h be the minimal height, t₀ the last time at which the height equals h and t₁ the first time from which on the height is at least h + 1. Between t₀ and t₁, the pieces along which the height increases and stays at most every later height are reflected by Module.preReflection x f, the equal-height excursions are kept, and the rest of the path after t₁ is translated by -x. It is none when f (π 1) - h < 1.

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

Littelmann's raising operator e_α on paths, the conjugate of TauCeti.PLPath.lower by the reversal of paths. Let h be the minimal height, t₁ the first time at which the height equals h and t₀ the last time up to which the height is at least h + 1. Between t₀ and t₁, the pieces along which the height decreases and stays at most every earlier height are reflected by Module.preReflection x f, the equal-height excursions are kept, and the rest of the path after t₁ is translated by x. It is none when -1 < h.

theorem TauCeti.PLPath.lower_ofSegments {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (l : List V) : lower f x (ofSegments 𝕜 l) = Option.map (ofSegments 𝕜) (listLower f x l)

The lowering operator may be computed on any presentation of a path.

theorem TauCeti.PLPath.raise_def {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (p : PLPath 𝕜 V) : raise f x p = Option.map reverse (lower f x p.reverse)

@[simp]

theorem TauCeti.PLPath.raise_reverse {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (p : PLPath 𝕜 V) : raise f x p.reverse = Option.map reverse (lower f x p)

@[simp]

theorem TauCeti.PLPath.lower_reverse {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V} (p : PLPath 𝕜 V) : lower f x p.reverse = Option.map reverse (raise f x p)

@[simp]

theorem TauCeti.PLPath.lower_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} : lower f x p = none ↔ f p.endpoint - minHeight f p < 1

The lowering operator is defined exactly when the final height exceeds the minimal height by at least 1.

@[simp]

theorem TauCeti.PLPath.raise_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} : raise f x p = none ↔ -1 < minHeight f p

The raising operator is defined exactly when the minimal height is at most -1.

theorem TauCeti.PLPath.endpoint_of_lower_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} (h : lower f x p = some q) : q.endpoint = p.endpoint - x

Lowering subtracts x from the endpoint.

theorem TauCeti.PLPath.endpoint_of_raise_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} (h : raise f x p = some q) : q.endpoint = p.endpoint + x

Raising adds x to the endpoint.

theorem TauCeti.PLPath.minHeight_of_lower_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} (hx : f x = 2) (h : lower f x p = some q) : minHeight f q = minHeight f p - 1

Lowering lowers the minimal height by one: min H(f_α π) = min H(π) - 1.

theorem TauCeti.PLPath.minHeight_of_raise_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} (hx : f x = 2) (h : raise f x p = some q) : minHeight f q = minHeight f p + 1

Raising raises the minimal height by one: min H(e_α π) = min H(π) + 1.

theorem TauCeti.PLPath.apply_endpoint_sub_minHeight_of_lower_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} (hx : f x = 2) (h : lower f x p = some q) : f q.endpoint - minHeight f q + 1 = f p.endpoint - minHeight f p

Lowering shortens the lowering string by one: H(1) - min H drops by one under f_α.

theorem TauCeti.PLPath.lower_straight {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {f : Module.Dual 𝕜 V} {x v : V} (h : 1 ≤ f v) : lower f x (straight 𝕜 v) = some (straight 𝕜 ((Module.preReflection x f) ((f v)⁻¹ • v)) * straight 𝕜 ((1 - (f v)⁻¹) • v))

Lowering the straight path t ↦ t • v with f v ≥ 1 reflects its initial piece, up to the time 1 / f v at which the height reaches 1.