Documentation

Mathlib.Combinatorics.Quiver.Path

Paths in quivers #

Given a quiver V, we define the type of paths from a : V to b : V as an inductive family. We define composition of paths and the action of prefunctors on paths.

inductive Quiver.Path {V : Type u} [Quiver V] (a : V) :
VSort (max (u + 1) v)

Path a b is the type of paths from a to b through the arrows of G.

Instances For
    def Quiver.Hom.toPath {V : Type u_1} [Quiver V] {a : V} {b : V} (e : a b) :

    An arrow viewed as a path of length one.

    Equations
    Instances For
      theorem Quiver.Path.nil_ne_cons {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) (e : b a) :
      Quiver.Path.nil Quiver.Path.cons p e
      theorem Quiver.Path.cons_ne_nil {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) (e : b a) :
      Quiver.Path.cons p e Quiver.Path.nil
      theorem Quiver.Path.obj_eq_of_cons_eq_cons {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b d} {e' : c d} (h : Quiver.Path.cons p e = Quiver.Path.cons p' e') :
      b = c
      theorem Quiver.Path.heq_of_cons_eq_cons {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b d} {e' : c d} (h : Quiver.Path.cons p e = Quiver.Path.cons p' e') :
      HEq p p'
      theorem Quiver.Path.hom_heq_of_cons_eq_cons {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b d} {e' : c d} (h : Quiver.Path.cons p e = Quiver.Path.cons p' e') :
      HEq e e'
      def Quiver.Path.length {V : Type u} [Quiver V] {a : V} {b : V} :

      The length of a path is the number of arrows it uses.

      Equations
      Instances For
        instance Quiver.Path.instInhabitedPath {V : Type u} [Quiver V] {a : V} :
        Equations
        • Quiver.Path.instInhabitedPath = { default := Quiver.Path.nil }
        @[simp]
        theorem Quiver.Path.length_nil {V : Type u} [Quiver V] {a : V} :
        Quiver.Path.length Quiver.Path.nil = 0
        @[simp]
        theorem Quiver.Path.length_cons {V : Type u} [Quiver V] (a : V) (b : V) (c : V) (p : Quiver.Path a b) (e : b c) :
        theorem Quiver.Path.eq_of_length_zero {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) (hzero : Quiver.Path.length p = 0) :
        a = b
        def Quiver.Path.comp {V : Type u} [Quiver V] {a : V} {b : V} {c : V} :
        Quiver.Path a bQuiver.Path b cQuiver.Path a c

        Composition of paths.

        Equations
        Instances For
          @[simp]
          theorem Quiver.Path.comp_cons {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (e : c d) :
          @[simp]
          theorem Quiver.Path.comp_nil {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) :
          Quiver.Path.comp p Quiver.Path.nil = p
          @[simp]
          theorem Quiver.Path.nil_comp {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) :
          Quiver.Path.comp Quiver.Path.nil p = p
          @[simp]
          theorem Quiver.Path.comp_assoc {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (r : Quiver.Path c d) :
          @[simp]
          theorem Quiver.Path.length_comp {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) :
          theorem Quiver.Path.comp_inj {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {p₁ : Quiver.Path a b} {p₂ : Quiver.Path a b} {q₁ : Quiver.Path b c} {q₂ : Quiver.Path b c} (hq : Quiver.Path.length q₁ = Quiver.Path.length q₂) :
          Quiver.Path.comp p₁ q₁ = Quiver.Path.comp p₂ q₂ p₁ = p₂ q₁ = q₂
          theorem Quiver.Path.comp_inj' {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {p₁ : Quiver.Path a b} {p₂ : Quiver.Path a b} {q₁ : Quiver.Path b c} {q₂ : Quiver.Path b c} (h : Quiver.Path.length p₁ = Quiver.Path.length p₂) :
          Quiver.Path.comp p₁ q₁ = Quiver.Path.comp p₂ q₂ p₁ = p₂ q₁ = q₂
          theorem Quiver.Path.comp_injective_left {V : Type u} [Quiver V] {a : V} {b : V} {c : V} (q : Quiver.Path b c) :
          theorem Quiver.Path.comp_injective_right {V : Type u} [Quiver V] {a : V} {b : V} {c : V} (p : Quiver.Path a b) :
          @[simp]
          theorem Quiver.Path.comp_inj_left {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {p₁ : Quiver.Path a b} {p₂ : Quiver.Path a b} {q : Quiver.Path b c} :
          Quiver.Path.comp p₁ q = Quiver.Path.comp p₂ q p₁ = p₂
          @[simp]
          theorem Quiver.Path.comp_inj_right {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {p : Quiver.Path a b} {q₁ : Quiver.Path b c} {q₂ : Quiver.Path b c} :
          Quiver.Path.comp p q₁ = Quiver.Path.comp p q₂ q₁ = q₂
          def Quiver.Path.toList {V : Type u} [Quiver V] {a : V} {b : V} :
          Quiver.Path a bList V

          Turn a path into a list. The list contains a at its head, but not b a priori.

          Equations
          Instances For
            @[simp]

            Quiver.Path.toList is a contravariant functor. The inversion comes from Quiver.Path and List having different preferred directions for adding elements.

            theorem Quiver.Path.toList_chain_nonempty {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) :
            List.Chain (fun x y => Nonempty (y x)) b (Quiver.Path.toList p)
            theorem Quiver.Path.toList_injective {V : Type u} [Quiver V] [∀ (a b : V), Subsingleton (a b)] (a : V) (b : V) :
            Function.Injective Quiver.Path.toList
            @[simp]
            theorem Quiver.Path.toList_inj {V : Type u} [Quiver V] {a : V} {b : V} [∀ (a b : V), Subsingleton (a b)] {p : Quiver.Path a b} {q : Quiver.Path a b} :
            def Prefunctor.mapPath {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {b : V} :
            Quiver.Path a bQuiver.Path (F.obj a) (F.obj b)

            The image of a path under a prefunctor.

            Equations
            Instances For
              @[simp]
              theorem Prefunctor.mapPath_nil {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) (a : V) :
              Prefunctor.mapPath F Quiver.Path.nil = Quiver.Path.nil
              @[simp]
              theorem Prefunctor.mapPath_cons {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {b : V} {c : V} (p : Quiver.Path a b) (e : b c) :
              @[simp]
              theorem Prefunctor.mapPath_comp {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) :
              @[simp]
              theorem Prefunctor.mapPath_toPath {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {b : V} (f : a b) :