Piecewise-linear paths up to reparametrization

Littelmann's path model works with piecewise-linear paths π : [0, 1] → V starting at π 0 = 0 in a vector space V over an ordered field 𝕜 (the weight space X ⊗ ℚ or X ⊗ ℝ of a root datum), identified up to nondecreasing surjective piecewise-linear reparametrization. A finite presentation of such a path is a subdivision 0 = t₀ ≤ t₁ ≤ ⋯ ≤ tₙ = 1 on whose pieces π is affine; it is recorded by its list of segments [v₁, …, vₙ], vₖ = π tₖ - π tₖ₋₁. The lengths tₖ - tₖ₋₁ are not recorded, since a reparametrization can change them at will. Two elementary moves change a presentation but are meant not to change the path it presents:

• a merge […, v, w, …] ↦ […, v + w, …] of two adjacent segments pointing in the same direction (SameRay 𝕜 v w), whose inverse subdivides a segment;
• the removal […, 0, …] ↦ […, …] of a stationary segment.

This file develops these presentations and their normal form. The algorithm TauCeti.PLPath.normalize removes the stationary segments and merges adjacent segments pointing in the same direction, using only the vector-space operations of V (so a presentation over ℚ stays over ℚ; no Euclidean arc length is involved). Its output is reduced, and two segment lists have the same normal form exactly when they are related by the elementary moves. The type TauCeti.PLPath 𝕜 V models paths by reduced segment lists, with Littelmann's concatenation π₁ * π₂ as a monoid structure, the endpoint π 1, and the reversed path t ↦ π (1 - t) - π 1.

This file works with segment lists only. The parametrized paths 𝕜 → V of presentations with durations (running over [0, duration p]), and the theorem that two presentations are reparametrizations of a common one exactly when their normal forms agree, are in TauCeti/RepresentationTheory/LSPath/Reparametrization.lean.

Main definitions

• TauCeti.PLPath.normalize: the normal form of a segment list, computed by TauCeti.PLPath.consMerge.
• TauCeti.PLPath.IsReduced: a segment list with no stationary segment and no two adjacent segments pointing in the same direction.
• TauCeti.PLPath.Move: the elementary moves between segment lists.
• TauCeti.PLPath: the model of piecewise-linear paths up to reparametrization by reduced segment lists.
• TauCeti.PLPath.ofSegments: the path presented by a segment list.
• TauCeti.PLPath.endpoint, TauCeti.PLPath.reverse, TauCeti.PLPath.straight: the endpoint, the reversed path and the straight path t ↦ t • v.
• TauCeti.PLPath.map: the linear image of a path, allowing collapsed segments.

Main results

• TauCeti.PLPath.normalize_eq_self_iff: a segment list is its own normal form exactly when it is reduced.
• TauCeti.PLPath.normalize_eq_normalize_iff, TauCeti.PLPath.ofSegments_eq_ofSegments_iff: two segment lists have the same normal form, that is define the same TauCeti.PLPath, exactly when they are related by the elementary moves.
• TauCeti.PLPath.ofSegments_append: concatenation of presentations presents the product.
• TauCeti.PLPath.endpoint_mul, TauCeti.PLPath.reverse_mul, TauCeti.PLPath.reverse_reverse: the endpoint is additive and reversal is an involutive anti-automorphism.
• TauCeti.PLPath.straight_add: a straight path along v + w, for v and w in the same ray, is the concatenation of the straight paths along v and along w.
• TauCeti.PLPath.straight_smul_mul_straight_smul, TauCeti.PLPath.ofSegments_smul_cons_smul_cons: subdividing a straight path, or a segment of a segment list, along a ray.
• TauCeti.PLPath.ofSegments_append_cut_eq: cutting a segment at a fraction θ ∈ [0, 1], in the middle of a segment list, does not change the presented path.
• TauCeti.PLPath.ofSegments_div_smul_cons_sub_div_smul_cons: subdividing a segment of a segment list at a fraction d / e with 0 ≤ d ≤ e.

References

• P. Littelmann, A Littlewood-Richardson rule for symmetrizable Kac-Moody algebras, Invent. Math. 116 (1994), §1.
• P. Littelmann, Paths and root operators in representation theory, Ann. of Math. 142 (1995), §1.

The normalization algorithm

noncomputable def TauCeti.PLPath.consMerge (𝕜 : Type u) {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) : List V → List V

Prepend the segment v to the segment list l, merging it into the first segment of l when the two point in the same direction, and dropping it when v = 0 and l is empty. This is the single step of TauCeti.PLPath.normalize.

noncomputable def TauCeti.PLPath.normalize (𝕜 : Type u) {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : List V

The normal form of a segment list: the stationary segments are removed and adjacent segments pointing in the same direction are merged, by prepending the segments one at a time with TauCeti.PLPath.consMerge.

structure TauCeti.PLPath.IsReduced (𝕜 : Type u) {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : Prop

A segment list is reduced if it has no stationary (zero) segment and no two adjacent segments point in the same direction. Reduced lists are the normal forms of TauCeti.PLPath.normalize.

• ne_zero (v : V) : v ∈ l → v ≠ 0

  No segment is stationary.

• isChain : List.IsChain (fun (v w : V) => ¬SameRay 𝕜 v w) l

  No two adjacent segments point in the same direction.

inductive TauCeti.PLPath.Move (𝕜 : Type u) {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : List V → List V → Prop

The elementary moves between segment lists, which change the presentation of a path but are meant not to change the path: merging two adjacent segments in the same ray (the inverse of subdividing a segment), and removing a stationary segment.

• merge {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l₁ l₂ : List V) {v w : V} : SameRay 𝕜 v w → Move 𝕜 (l₁ ++ v :: w :: l₂) (l₁ ++ (v + w) :: l₂)

  Merge two adjacent segments pointing in the same direction.

• erase_zero {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l₁ l₂ : List V) : Move 𝕜 (l₁ ++ 0 :: l₂) (l₁ ++ l₂)

  Remove a stationary segment.

@[simp]

theorem TauCeti.PLPath.consMerge_zero {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : consMerge 𝕜 0 l = l

theorem TauCeti.PLPath.consMerge_nil_of_ne_zero {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v : V} (hv : v ≠ 0) : consMerge 𝕜 v [] = [v]

theorem TauCeti.PLPath.consMerge_cons_of_sameRay {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v w : V} {l : List V} (h : SameRay 𝕜 v w) : consMerge 𝕜 v (w :: l) = (v + w) :: l

theorem TauCeti.PLPath.consMerge_cons_of_not_sameRay {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v w : V} {l : List V} (h : ¬SameRay 𝕜 v w) : consMerge 𝕜 v (w :: l) = v :: w :: l

theorem TauCeti.PLPath.consMerge_consMerge {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v w : V} (h : SameRay 𝕜 v w) (l : List V) : consMerge 𝕜 v (consMerge 𝕜 w l) = consMerge 𝕜 (v + w) l

Prepending two segments in the same ray one after the other is the same as prepending their sum.

@[simp]

theorem TauCeti.PLPath.normalize_nil {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : normalize 𝕜 [] = []

@[simp]

theorem TauCeti.PLPath.normalize_cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) (l : List V) : normalize 𝕜 (v :: l) = consMerge 𝕜 v (normalize 𝕜 l)

theorem TauCeti.PLPath.normalize_append {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l₁ l₂ : List V) : normalize 𝕜 (l₁ ++ l₂) = List.foldr (consMerge 𝕜) (normalize 𝕜 l₂) l₁

@[simp]

theorem TauCeti.PLPath.normalize_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : normalize 𝕜 (normalize 𝕜 l) = normalize 𝕜 l

@[simp]

theorem TauCeti.PLPath.normalize_normalize_append {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l₁ l₂ : List V) : normalize 𝕜 (normalize 𝕜 l₁ ++ l₂) = normalize 𝕜 (l₁ ++ l₂)

@[simp]

theorem TauCeti.PLPath.normalize_append_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l₁ l₂ : List V) : normalize 𝕜 (l₁ ++ normalize 𝕜 l₂) = normalize 𝕜 (l₁ ++ l₂)

@[simp]

theorem TauCeti.PLPath.sum_consMerge {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) (l : List V) : (consMerge 𝕜 v l).sum = v + l.sum

Prepending a segment with TauCeti.PLPath.consMerge adds it to the endpoint.

@[simp]

theorem TauCeti.PLPath.sum_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : (normalize 𝕜 l).sum = l.sum

Normalization preserves the endpoint v₁ + ⋯ + vₙ of a presentation.

@[simp]

theorem TauCeti.PLPath.consMerge_eq_nil_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v : V} {l : List V} : consMerge 𝕜 v l = [] ↔ v = 0 ∧ l = []

@[simp]

theorem TauCeti.PLPath.normalize_eq_nil_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l : List V} : normalize 𝕜 l = [] ↔ ∀ v ∈ l, v = 0

The normal form of a segment list is empty exactly when every segment is stationary.

Reduced segment lists

@[simp]

theorem TauCeti.PLPath.isReduced_nil {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : IsReduced 𝕜 []

theorem TauCeti.PLPath.isReduced_cons_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v : V} {l : List V} : IsReduced 𝕜 (v :: l) ↔ v ≠ 0 ∧ (∀ w ∈ l.head?, ¬SameRay 𝕜 v w) ∧ IsReduced 𝕜 l

theorem TauCeti.PLPath.IsReduced.consMerge {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l : List V} (h : IsReduced 𝕜 l) (v : V) : IsReduced 𝕜 (PLPath.consMerge 𝕜 v l)

theorem TauCeti.PLPath.isReduced_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : IsReduced 𝕜 (normalize 𝕜 l)

theorem TauCeti.PLPath.mem_of_mem_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l : List V} {T : Set V} (hT : ∀ v ∈ T, ∀ w ∈ T, SameRay 𝕜 v w → v + w ∈ T) (hl : ∀ v ∈ l, v ≠ 0 → v ∈ T) {v : V} (hv : v ∈ normalize 𝕜 l) : v ∈ T

Normalization only merges segments in the same ray and drops stationary ones. So if a set T contains v + w for all v, w ∈ T in the same ray, and contains every nonstationary segment of l, then it contains every segment of normalize 𝕜 l.

theorem TauCeti.PLPath.IsReduced.normalize_eq {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l : List V} (h : IsReduced 𝕜 l) : normalize 𝕜 l = l

theorem TauCeti.PLPath.normalize_eq_self_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l : List V} : normalize 𝕜 l = l ↔ IsReduced 𝕜 l

A segment list is its own normal form exactly when it is reduced.

theorem TauCeti.PLPath.IsReduced.reverse_map_neg {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l : List V} (h : IsReduced 𝕜 l) : IsReduced 𝕜 (List.map Neg.neg l).reverse

Reversing the order of the segments and negating them preserves reducedness.

Elementary moves

theorem TauCeti.PLPath.Move.cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l₁ l₂ : List V} (h : Move 𝕜 l₁ l₂) (v : V) : Move 𝕜 (v :: l₁) (v :: l₂)

theorem TauCeti.PLPath.Move.reverse_map_neg {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l₁ l₂ : List V} (h : Move 𝕜 l₁ l₂) : Move 𝕜 (List.map Neg.neg l₁).reverse (List.map Neg.neg l₂).reverse

theorem TauCeti.PLPath.Move.normalize_eq {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l₁ l₂ : List V} (h : Move 𝕜 l₁ l₂) : normalize 𝕜 l₁ = normalize 𝕜 l₂

An elementary move does not change the normal form.

theorem TauCeti.PLPath.reflTransGen_move_consMerge {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) (l : List V) : Relation.ReflTransGen (Move 𝕜) (v :: l) (consMerge 𝕜 v l)

Prepending a segment with TauCeti.PLPath.consMerge is a sequence of elementary moves.

theorem TauCeti.PLPath.reflTransGen_move_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : Relation.ReflTransGen (Move 𝕜) l (normalize 𝕜 l)

Every segment list is connected to its normal form by elementary moves.

theorem TauCeti.PLPath.normalize_eq_normalize_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l₁ l₂ : List V} : normalize 𝕜 l₁ = normalize 𝕜 l₂ ↔ Relation.EqvGen (Move 𝕜) l₁ l₂

Two segment lists have the same normal form exactly when they are related by elementary moves: the normal form is a complete invariant for the elementary moves.

theorem TauCeti.PLPath.normalize_reverse_map_neg {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : normalize 𝕜 (List.map Neg.neg l).reverse = (List.map Neg.neg (normalize 𝕜 l)).reverse

structure TauCeti.PLPath (𝕜 : Type u) (V : Type v) [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : Type v

A model of piecewise-linear paths π : [0, 1] → V with π 0 = 0, up to nondecreasing surjective piecewise-linear reparametrization, by reduced segment lists: a path is meant to be recorded by the successive displacements along its maximal straight pieces. See TauCeti.PLPath.ofSegments for the path presented by an arbitrary segment list, and TauCeti.PLPath.ofSegments_map_snd_eq_iff_exists_isReparam for the comparison with parametrized paths.

• segments : List V

  The segments of the path, in order.

• isReduced : IsReduced 𝕜 self.segments

  The segment list is reduced.

theorem TauCeti.PLPath.ext_iff {𝕜 : Type u} {V : Type v} {inst✝ : Field 𝕜} {inst✝¹ : PartialOrder 𝕜} {inst✝² : IsStrictOrderedRing 𝕜} {inst✝³ : AddCommGroup V} {inst✝⁴ : Module 𝕜 V} {x y : PLPath 𝕜 V} : x = y ↔ x.segments = y.segments

theorem TauCeti.PLPath.ext {𝕜 : Type u} {V : Type v} {inst✝ : Field 𝕜} {inst✝¹ : PartialOrder 𝕜} {inst✝² : IsStrictOrderedRing 𝕜} {inst✝³ : AddCommGroup V} {inst✝⁴ : Module 𝕜 V} {x y : PLPath 𝕜 V} (segments : x.segments = y.segments) : x = y

Paths presented by segment lists

noncomputable def TauCeti.PLPath.ofSegments (𝕜 : Type u) {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : PLPath 𝕜 V

The path presented by a segment list: it traverses the segments in order.

noncomputable def TauCeti.PLPath.straight (𝕜 : Type u) {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) : PLPath 𝕜 V

The straight path t ↦ t • v.

theorem TauCeti.PLPath.straight_def {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) : straight 𝕜 v = ofSegments 𝕜 [v]

@[simp]

theorem TauCeti.PLPath.segments_ofSegments {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : (ofSegments 𝕜 l).segments = normalize 𝕜 l

@[simp]

theorem TauCeti.PLPath.ofSegments_segments {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : ofSegments 𝕜 p.segments = p

theorem TauCeti.PLPath.ofSegments_surjective {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : Function.Surjective (ofSegments 𝕜)

theorem TauCeti.PLPath.ofSegments_eq_ofSegments_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l₁ l₂ : List V} : ofSegments 𝕜 l₁ = ofSegments 𝕜 l₂ ↔ Relation.EqvGen (Move 𝕜) l₁ l₂

Two segment lists define the same TauCeti.PLPath, that is have the same normal form, exactly when they are related by elementary moves.

Concatenation

@[instance_reducible]

instance TauCeti.PLPath.instOne {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : One (PLPath 𝕜 V)

The constant path at 0.

@[instance_reducible]

noncomputable instance TauCeti.PLPath.instMul {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : Mul (PLPath 𝕜 V)

Littelmann's concatenation π₁ * π₂: traverse π₁, then the translate of π₂ by the endpoint of π₁.

@[simp]

theorem TauCeti.PLPath.segments_one {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : segments 1 = []

@[simp]

theorem TauCeti.PLPath.segments_mul {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p q : PLPath 𝕜 V) : (p * q).segments = normalize 𝕜 (p.segments ++ q.segments)

@[simp]

theorem TauCeti.PLPath.ofSegments_nil {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : ofSegments 𝕜 [] = 1

@[simp]

theorem TauCeti.PLPath.ofSegments_eq_one_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {l : List V} : ofSegments 𝕜 l = 1 ↔ ∀ v ∈ l, v = 0

A segment list presents the constant path exactly when every segment is stationary.

@[simp]

theorem TauCeti.PLPath.ofSegments_append {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l₁ l₂ : List V) : ofSegments 𝕜 (l₁ ++ l₂) = ofSegments 𝕜 l₁ * ofSegments 𝕜 l₂

@[instance_reducible]

noncomputable instance TauCeti.PLPath.instMonoid {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : Monoid (PLPath 𝕜 V)

theorem TauCeti.PLPath.ofSegments_cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) (l : List V) : ofSegments 𝕜 (v :: l) = straight 𝕜 v * ofSegments 𝕜 l

A path presented by v :: l is the straight path along v followed by the path presented by l.

@[simp]

theorem TauCeti.PLPath.ofSegments_zero_cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : ofSegments 𝕜 (0 :: l) = ofSegments 𝕜 l

A stationary first segment does not change the presented path.

theorem TauCeti.PLPath.prod_map_straight {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : (List.map (straight 𝕜) l).prod = ofSegments 𝕜 l

Every path is the concatenation of the straight paths along its segments.

The endpoint

def TauCeti.PLPath.endpoint {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : V

The endpoint π 1 of a path, the sum of its segments.

theorem TauCeti.PLPath.endpoint_def {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : p.endpoint = p.segments.sum

@[simp]

theorem TauCeti.PLPath.endpoint_ofSegments {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : (ofSegments 𝕜 l).endpoint = l.sum

@[simp]

theorem TauCeti.PLPath.endpoint_one {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : endpoint 1 = 0

@[simp]

theorem TauCeti.PLPath.endpoint_mul {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p q : PLPath 𝕜 V) : (p * q).endpoint = p.endpoint + q.endpoint

Reversal

def TauCeti.PLPath.reverse {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : PLPath 𝕜 V

The reversed path t ↦ π (1 - t) - π 1: its segments are those of π, negated and in the opposite order.

@[simp]

theorem TauCeti.PLPath.segments_reverse {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : p.reverse.segments = (List.map Neg.neg p.segments).reverse

@[simp]

theorem TauCeti.PLPath.reverse_ofSegments {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (l : List V) : (ofSegments 𝕜 l).reverse = ofSegments 𝕜 (List.map Neg.neg l).reverse

@[simp]

theorem TauCeti.PLPath.reverse_reverse {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : p.reverse.reverse = p

theorem TauCeti.PLPath.reverse_involutive {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : Function.Involutive reverse

@[simp]

theorem TauCeti.PLPath.reverse_one {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : reverse 1 = 1

@[simp]

theorem TauCeti.PLPath.reverse_mul {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p q : PLPath 𝕜 V) : (p * q).reverse = q.reverse * p.reverse

@[simp]

theorem TauCeti.PLPath.endpoint_reverse {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : p.reverse.endpoint = -p.endpoint

Straight paths

theorem TauCeti.PLPath.segments_straight_of_ne_zero {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v : V} (hv : v ≠ 0) : (straight 𝕜 v).segments = [v]

@[simp]

theorem TauCeti.PLPath.straight_zero {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] : straight 𝕜 0 = 1

@[simp]

theorem TauCeti.PLPath.endpoint_straight {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) : (straight 𝕜 v).endpoint = v

@[simp]

theorem TauCeti.PLPath.reverse_straight {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (v : V) : (straight 𝕜 v).reverse = straight 𝕜 (-v)

theorem TauCeti.PLPath.straight_add {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v w : V} (h : SameRay 𝕜 v w) : straight 𝕜 (v + w) = straight 𝕜 v * straight 𝕜 w

Subdivision: the straight path along v + w, for v and w in the same ray, is the straight path along v followed by the straight path along w.

theorem TauCeti.PLPath.straight_smul_mul_straight_smul {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (w : V) : straight 𝕜 (a • w) * straight 𝕜 (b • w) = straight 𝕜 ((a + b) • w)

Subdivision along a ray: for 0 ≤ a and 0 ≤ b, the straight path along a • w followed by the straight path along b • w is the straight path along (a + b) • w.

@[simp]

theorem TauCeti.PLPath.straight_natCast_smul {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (n : ℕ) (v : V) : straight 𝕜 (↑n • v) = straight 𝕜 v ^ n

A straight path along a natural multiple is the concatenation power of the original straight path.

theorem TauCeti.PLPath.ofSegments_smul_cons_smul_cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (w : V) (l : List V) : ofSegments 𝕜 (a • w :: b • w :: l) = ofSegments 𝕜 ((a + b) • w :: l)

Subdividing a segment along its ray does not change the presented path: for 0 ≤ a and 0 ≤ b, the segments a • w and b • w present the same path as the single segment (a + b) • w.

theorem TauCeti.PLPath.ofSegments_append_cut_eq {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {a m r : List V} {v : V} {θ : 𝕜} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : ofSegments 𝕜 (a ++ (m ++ [θ • v]) ++ (1 - θ) • v :: r) = ofSegments 𝕜 (a ++ m ++ v :: r)

Cutting a segment v of a path at the fraction θ ∈ [0, 1], in the middle of the segments a ++ m ++ v :: r, does not change the path presented by the segments.

theorem TauCeti.PLPath.ofSegments_div_smul_cons_sub_div_smul_cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] [PosMulReflectLT 𝕜] {d e : 𝕜} (hd : 0 ≤ d) (hde : d ≤ e) (he : 0 < e) (w : V) (l : List V) : ofSegments 𝕜 ((d / e) • w :: ((e - d) / e) • w :: l) = ofSegments 𝕜 (w :: l)

Subdividing a segment w at the fraction d / e, for 0 ≤ d ≤ e and 0 < e, into the segments (d / e) • w and ((e - d) / e) • w does not change the presented path.

Linear images

theorem TauCeti.PLPath.Move.map {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] {l m : List V} (h : Move 𝕜 l m) (g : V →ₗ[𝕜] W) : Move 𝕜 (List.map (⇑g) l) (List.map (⇑g) m)

Taking a linear image preserves elementary path moves, including when segments collapse.

theorem TauCeti.PLPath.ofSegments_map_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (g : V →ₗ[𝕜] W) (l : List V) : ofSegments 𝕜 (List.map (⇑g) (normalize 𝕜 l)) = ofSegments 𝕜 (List.map (⇑g) l)

Normalizing a presentation before taking its linear image does not change the path.

noncomputable def TauCeti.PLPath.map {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (p : PLPath 𝕜 V) (g : V →ₗ[𝕜] W) : PLPath 𝕜 W

The linear image of a piecewise-linear path, with any collapsed segments removed.

theorem TauCeti.PLPath.map_def {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (p : PLPath 𝕜 V) (g : V →ₗ[𝕜] W) : p.map g = ofSegments 𝕜 (List.map (⇑g) p.segments)

@[simp]

theorem TauCeti.PLPath.map_ofSegments {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (l : List V) (g : V →ₗ[𝕜] W) : (ofSegments 𝕜 l).map g = ofSegments 𝕜 (List.map (⇑g) l)

A linear image can be computed on any segment presentation.

@[simp]

theorem TauCeti.PLPath.map_id {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : PLPath 𝕜 V) : p.map LinearMap.id = p

@[simp]

theorem TauCeti.PLPath.map_map {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} {U : Type u_2} [AddCommGroup W] [Module 𝕜 W] [AddCommGroup U] [Module 𝕜 U] (p : PLPath 𝕜 V) (g : V →ₗ[𝕜] W) (h : W →ₗ[𝕜] U) : (p.map g).map h = p.map (h ∘ₗ g)

Linear images respect composition.

@[simp]

theorem TauCeti.PLPath.map_one {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (g : V →ₗ[𝕜] W) : map 1 g = 1

@[simp]

theorem TauCeti.PLPath.map_mul {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (p q : PLPath 𝕜 V) (g : V →ₗ[𝕜] W) : (p * q).map g = p.map g * q.map g

Linear images preserve concatenation.

@[simp]

theorem TauCeti.PLPath.map_straight {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (v : V) (g : V →ₗ[𝕜] W) : (straight 𝕜 v).map g = straight 𝕜 (g v)

@[simp]

theorem TauCeti.PLPath.endpoint_map {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (p : PLPath 𝕜 V) (g : V →ₗ[𝕜] W) : (p.map g).endpoint = g p.endpoint

@[simp]

theorem TauCeti.PLPath.map_reverse {𝕜 : Type u} {V : Type v} [Field 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {W : Type u_1} [AddCommGroup W] [Module 𝕜 W] (p : PLPath 𝕜 V) (g : V →ₗ[𝕜] W) : p.reverse.map g = (p.map g).reverse

Linear images commute with reversal.