Documentation

TauCeti.RepresentationTheory.Quiver.LastArrow

The last arrow of a path #

A path i → b in a quiver is either trivial, which forces i = b, or a path i → a followed by a last arrow a ⟶ b. This file records that dichotomy as an equivalence and reads off the resulting recursion for the number of paths out of a fixed vertex.

Main definitions #

Main results #

Implementation notes #

The equivalence is the constructor dichotomy of Quiver.Path: Quiver.Path.nil is the left summand and Quiver.Path.cons the right one, so both directions are definitional matches. The proposition i = b is wrapped in PLift only to make the summand a type, so that Nat.card applies. The simp lemmas TauCeti.pathLastArrowEquiv_nil, TauCeti.pathLastArrowEquiv_cons, TauCeti.pathLastArrowEquiv_symm_inl and TauCeti.pathLastArrowEquiv_symm_inr record those matches on both summands, so consumers compute with the equivalence without unfolding it. Their proofs are written (rfl) rather than rfl: the parenthesised form keeps the proof opaque to the module system, so the equivalence itself need not be @[expose]d.

The dual decomposition, by the first arrow of a path, is not available in this form: the recursion of Quiver.Path is on the target vertex, so the first arrow is not visible to a match. It is built instead by an explicit recursion over the path, in TauCeti.RepresentationTheory.Quiver.FirstArrow.

References #

The path count is the combinatorial input to the Euler-form identity for the projective representation at a vertex, Layer 4 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md.

source
def TauCeti.pathLastArrowEquiv {V : Type u} [Quiver V] (i b : V) :
Quiver.Path i b ≃ PLift (i = b) ⊕ (a : V) × Quiver.Path i a × (a ⟶ b)

The last-arrow decomposition of a path. A path i → b is either trivial, and then i = b, or a path i → a followed by a last arrow a ⟶ b, uniquely so.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.pathLastArrowEquiv_nil {V : Type u} [Quiver V] (i : V) :
    (pathLastArrowEquiv i i) Quiver.Path.nil = Sum.inl { down := ⋯ }

    The trivial path is the left summand of the last-arrow decomposition.

    source
    @[simp]
    theorem TauCeti.pathLastArrowEquiv_cons {V : Type u} [Quiver V] {i a b : V} (p : Quiver.Path i a) (e : a ⟶ b) :
    (pathLastArrowEquiv i b) (p.cons e) = Sum.inr ⟨a, (p, e)⟩

    A path with a last arrow is the right summand of the last-arrow decomposition.

    source
    @[simp]
    theorem TauCeti.pathLastArrowEquiv_symm_inl {V : Type u} [Quiver V] (i : V) :
    (pathLastArrowEquiv i i).symm (Sum.inl { down := ⋯ }) = Quiver.Path.nil

    The left summand of the last-arrow decomposition recomposes to the trivial path.

    source
    @[simp]
    theorem TauCeti.pathLastArrowEquiv_symm_inr {V : Type u} [Quiver V] {i b : V} (a : V) (p : Quiver.Path i a) (e : a ⟶ b) :
    (pathLastArrowEquiv i b).symm (Sum.inr ⟨a, (p, e)⟩) = p.cons e

    The right summand of the last-arrow decomposition recomposes by appending the last arrow.

    source
    theorem TauCeti.card_path_eq_ite_add_sum_lastArrow {V : Type u} [Quiver V] [DecidableEq V] [Fintype V] (i : V) [∀ (a : V), Finite (Quiver.Path i a)] (b : V) [∀ (a : V), Finite (a ⟶ b)] :
    Nat.card (Quiver.Path i b) = (if i = b then 1 else 0) + ∑ a : V, Nat.card (Quiver.Path i a) * Nat.card (a ⟶ b)

    The last-arrow recursion for path counts. The paths i → b are the trivial one, present exactly when i = b, together with a path i → a and an arrow a ⟶ b. All three cardinalities are honest counts only when the paths out of i are finite, which is what the hypothesis [∀ a, Finite (Quiver.Path i a)] provides. The only arrows counted are those into b, so [∀ a, Finite (a ⟶ b)] suffices for the arrow factors.

    This is the mirror image of TauCeti.card_path_eq_ite_add_sum_firstArrow.