Path Vertices

This file provides lemmas for reasoning about the vertices of a path.

def Quiver.Path.end {V : Type u_1} [Quiver V] {a b : V} : Path a b → V

The end vertex of a path. A path p : Path a b has p.end = b.

@[simp]

theorem Quiver.Path.end_cons {V : Type u_1} [Quiver V] {a b c : V} (p : Path a b) (e : b ⟶ c) : (p.cons e).end = c

def Quiver.Path.vertices {V : Type u_1} [Quiver V] {a b : V} : Path a b → List V

The list of vertices in a path, including the start and end vertices.

@[simp]

theorem Quiver.Path.vertices_nil {V : Type u_1} [Quiver V] (a : V) : nil.vertices = [a]

@[simp]

theorem Quiver.Path.vertices_cons {V : Type u_1} [Quiver V] {a b c : V} (p : Path a b) (e : b ⟶ c) : (p.cons e).vertices = p.vertices.concat c

theorem Quiver.Path.mem_vertices_cons {V : Type u_1} [Quiver V] {a b c : V} (p : Path a b) (e : b ⟶ c) {x : V} : x ∈ (p.cons e).vertices ↔ x ∈ p.vertices ∨ x = c

The vertex list of cons — convenient simp form.

theorem Quiver.Path.verticesSet_nil {V : Type u_1} [Quiver V] {a : V} : {v : V | v ∈ nil.vertices} = {a}

@[simp]

theorem Quiver.Path.vertices_length {V : Type u_2} [Quiver V] {a b : V} (p : Path a b) : p.vertices.length = p.length + 1

The length of vertices list equals path length plus one

theorem Quiver.Path.length_vertices_pos {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : 0 < p.vertices.length

theorem Quiver.Path.vertices_ne_nil {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : p.vertices ≠ []

theorem Quiver.Path.start_mem_vertices {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : a ∈ p.vertices

@[simp]

theorem Quiver.Path.vertices_head? {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : p.vertices.head? = some a

The head of the vertices list is the start vertex

@[simp]

theorem Quiver.Path.vertices_head_eq {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) (h : p.vertices ≠ [] := ⋯) : p.vertices.head h = a

The head of the vertices list is the start vertex.

@[simp]

theorem Quiver.Path.getElem_vertices_zero {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : p.vertices[0] = a

@[simp]

theorem Quiver.Path.vertices_getLast {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) (h : p.vertices ≠ [] := ⋯) : p.vertices.getLast h = b

@[simp]

theorem Quiver.Path.dropLast_append_end_eq {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : p.vertices.dropLast ++ [b] = p.vertices

@[simp]

theorem Quiver.Path.vertices_comp {V : Type u_1} [Quiver V] {a b c : V} (p : Path a b) (q : Path b c) : (p.comp q).vertices = p.vertices.dropLast ++ q.vertices

@[simp]

theorem Quiver.Path.length_eq_zero_iff {V : Type u_1} [Quiver V] {a : V} (p : Path a a) : p.length = 0 ↔ p = nil

theorem Quiver.Path.vertices_comp_get_length_eq {V : Type u_1} [Quiver V] {a b c : V} (p₁ : Path a c) (p₂ : Path c b) (h : p₁.length < (p₁.comp p₂).vertices.length := by simp) : (p₁.comp p₂).vertices.get ⟨p₁.length, h⟩ = c

@[simp]

theorem Quiver.Path.vertices_toPath {V : Type u_1} [Quiver V] {i j : V} (e : i ⟶ j) : e.toPath.vertices = [i, j]

theorem Quiver.Path.vertices_toPath_tail {V : Type u_1} [Quiver V] {i j : V} (e : i ⟶ j) : e.toPath.vertices.tail = [j]

theorem Quiver.Path.nil_of_comp_eq_nil_left {V : Type u_1} [Quiver V] {a b : V} {p : Path a b} {q : Path b a} (h : p.comp q = nil) : p.length = 0

If a composition is nil, the left component must be nil (proved via lengths, avoiding dependent pattern-matching).

theorem Quiver.Path.nil_of_comp_eq_nil_right {V : Type u_1} [Quiver V] {a b : V} {p : Path a b} {q : Path b a} (h : p.comp q = nil) : q.length = 0

If a composition is nil, the right component must be nil

theorem Quiver.Path.comp_eq_nil_iff {V : Type u_1} [Quiver V] {a b : V} {p : Path a b} {q : Path b a} : p.comp q = nil ↔ p.length = 0 ∧ q.length = 0

@[simp]

theorem Quiver.Path.end_mem_vertices {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : b ∈ p.vertices

Path vertices decomposition

theorem Quiver.Path.exists_eq_comp_of_le_length {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) {n : ℕ} (hn : n ≤ p.length) : ∃ (v : V) (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂ ∧ p₁.length = n

Given a path p : Path a b and an index n ≤ p.length, we can split p = p₁.comp p₂ with p₁.length = n.

theorem Quiver.Path.exists_eq_comp_and_length_eq_of_lt_length {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) (n : ℕ) (hn : n < p.vertices.length) : ∃ (v : V) (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂ ∧ p₁.length = n ∧ v = p.vertices[n]

split_at_vertex decomposes a path p at the vertex sitting in position i of its vertices

theorem Quiver.Path.exists_eq_comp_of_mem_vertices {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) {v : V} (hv : v ∈ p.vertices) : ∃ (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂

If a vertex v occurs in the list of vertices of a path p : Path a b, then p can be decomposed as a concatenation of a subpath from a to v and a subpath from v to b.

theorem Quiver.Path.exists_eq_comp_and_notMem_tail_of_mem_vertices {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) {v : V} (hv : v ∈ p.vertices) : ∃ (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail

Split a path at the last occurrence of a vertex.