Documentation

Mathlib.Combinatorics.Quiver.Path.Vertices

Path Vertices #

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

source
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
Instances For
    source
    @[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
    source
    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
    Instances For
      source
      @[simp]
      theorem Quiver.Path.vertices_nil {V : Type u_1} [Quiver V] (a : V) :
      nil.vertices = [a]
      source
      @[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
      source
      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.

      source
      theorem Quiver.Path.verticesSet_nil {V : Type u_1} [Quiver V] {a : V} :
      {v : V | v ∈ nil.vertices} = {a}
      source
      @[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

      source
      theorem Quiver.Path.length_vertices_pos {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) :
      0 < p.vertices.length
      source
      theorem Quiver.Path.vertices_ne_nil {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) :
      p.vertices ≠ []
      source
      theorem Quiver.Path.start_mem_vertices {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) :
      a ∈ p.vertices
      source
      @[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

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

      source
      @[simp]
      theorem Quiver.Path.getElem_vertices_zero {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) :
      p.vertices[0] = a
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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
      source
      @[simp]
      theorem Quiver.Path.vertices_toPath {V : Type u_1} [Quiver V] {i j : V} (e : i ⟶ j) :
      e.toPath.vertices = [i, j]
      source
      theorem Quiver.Path.vertices_toPath_tail {V : Type u_1} [Quiver V] {i j : V} (e : i ⟶ j) :
      e.toPath.vertices.tail = [j]
      source
      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).

      source
      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

      source
      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
      source
      @[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 #

      source
      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.

      source
      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

      source
      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.

      source
      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.