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.

Equations

• x✝.end = x✝¹

@[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.

Equations

• Quiver.Path.nil.vertices = [a]
• (p.cons e).vertices = p.vertices.concat (p.cons e).end

@[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 ≠ []

@[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.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.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

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.length_eq_zero_iff {V : Type u_1} [Quiver V] {a : V} (p : Path a a) : p.length = 0 ↔ p = nil

@[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.

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

The last element of the vertices list is the end vertex.

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