Documentation

TauCeti.Combinatorics.Quiver.TotalPath

Indexed quiver paths and partial concatenation #

TauCeti.Quiver.TotalPath Q records a path of a quiver together with its source and target. Two such paths can be concatenated when the target of the second is the source of the first. The partial operation TauCeti.Quiver.TotalPath.mul? records this condition with an Option result, using the later-factor-first order: x.mul? y traces y and then x.

Concatenation adds path lengths and is associative as a partial operation. Trivial paths are left and right units at the appropriate endpoints. These operations supply the path index and multiplication of the path algebra, independently of any coefficient semiring.

Main definitions #

Main results #

References #

Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II.

source
@[reducible, inline]
abbrev TauCeti.Quiver.TotalPath (Q : Type u) [Quiver Q] :
Type (max u v)

The total space of the paths of a quiver: a path together with its source and target. This is the index type of the path basis of the path algebra.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Quiver.TotalPath.eq_nil_iff {Q : Type u} [Quiver Q] {v : Q} {x : TotalPath Q} :
    x = ⟨v, ⟨v, Quiver.Path.nil⟩⟩ ↔ x.fst = v ∧ x.snd.snd.length = 0

    An indexed path is the trivial path at v exactly when it starts at v and has length zero. Stated this way the equality is checked against two non-dependent conditions, so recognizing a trivial path inside a concatenation needs no transport along the endpoints.

    source
    noncomputable def TauCeti.Quiver.TotalPath.mul? {Q : Type u} [Quiver Q] (x y : TotalPath Q) :
    Option (TotalPath Q)

    Concatenation of indexed paths in the later factor first order used by the path algebra: x.mul? y traces y and then x, and is none unless y ends where x starts.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Quiver.TotalPath.mul?_mk {Q : Type u} [Quiver Q] {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a) :
      mul? ⟨a, ⟨b, p⟩⟩ ⟨c, ⟨a, q⟩⟩ = some ⟨c, ⟨b, q.comp p⟩⟩

      Composable indexed paths concatenate, the later factor written first.

      source
      theorem TauCeti.Quiver.TotalPath.mul?_eq_none {Q : Type u} [Quiver Q] {x y : TotalPath Q} (h : y.snd.fst ≠ x.fst) :
      x.mul? y = none

      Indexed paths that do not meet have no concatenation.

      source
      theorem TauCeti.Quiver.TotalPath.mul?_eq_none_iff {Q : Type u} [Quiver Q] {x y : TotalPath Q} :
      x.mul? y = none ↔ y.snd.fst ≠ x.fst

      The concatenation of two indexed paths is undefined exactly when they do not meet.

      source
      theorem TauCeti.Quiver.TotalPath.length_eq_add_of_mul?_eq_some {Q : Type u} [Quiver Q] {x y z : TotalPath Q} (h : x.mul? y = some z) :
      z.snd.snd.length = x.snd.snd.length + y.snd.snd.length

      Concatenation adds lengths: a path produced by mul? is as long as its two factors together.

      source
      @[simp]
      theorem TauCeti.Quiver.TotalPath.mul?_nil_left {Q : Type u} [Quiver Q] (x : TotalPath Q) :
      mul? ⟨x.snd.fst, ⟨x.snd.fst, Quiver.Path.nil⟩⟩ x = some x

      The trivial path at the target of x is a left unit for x.

      source
      @[simp]
      theorem TauCeti.Quiver.TotalPath.mul?_nil_right {Q : Type u} [Quiver Q] (x : TotalPath Q) :
      x.mul? ⟨x.fst, ⟨x.fst, Quiver.Path.nil⟩⟩ = some x

      The trivial path at the source of x is a right unit for x.

      source
      theorem TauCeti.Quiver.TotalPath.mul?_assoc {Q : Type u} [Quiver Q] (x y z : TotalPath Q) :
      ((x.mul? y).bind fun (w : TotalPath Q) => w.mul? z) = (y.mul? z).bind fun (w : TotalPath Q) => x.mul? w

      Concatenation of indexed paths is associative as a partial operation.

      source
      theorem TauCeti.Quiver.TotalPath.mk_cons_eq_mk_cons_iff {Q : Type u} [Quiver Q] {s s' i i' j : Q} {p : Quiver.Path s i} {p' : Quiver.Path s' i'} {b : i ⟶ j} {b' : i' ⟶ j} :
      ⟨s', ⟨j, p'.cons b'⟩⟩ = ⟨s, ⟨j, p.cons b⟩⟩ ↔ ⟨s', ⟨i', p'⟩⟩ = ⟨s, ⟨i, p⟩⟩ ∧ ⟨i', b'⟩ = ⟨i, b⟩

      A path into j is determined by its last arrow and the path before it: two indexed paths ending in arrows into j agree exactly when their prefixes and their last arrows do.