The first arrow of a path

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

It is the mirror image of TauCeti.RepresentationTheory.Quiver.LastArrow, which decomposes a path by its last arrow instead, and the two feed the two sides of the Euler form of a finite quiver.

Main definitions

• TauCeti.pathFirstArrowEquiv: the first-arrow decomposition Path a j ≃ PLift (a = j) ⊕ Σ b, (a ⟶ b) × Path b j.

Main results

• TauCeti.exists_hom_mem_path_vertices_of_mem_dropLast: every occurrence in a path's vertex list except its final occurrence is the source of an arrow landing on the path.
• TauCeti.exists_hom_mem_path_vertices: every vertex visited by a nontrivial closed path is the source of an arrow landing on the path.
• TauCeti.card_path_eq_ite_add_sum_firstArrow: the path count #(a → j) equals ∑_b #(a ⟶ b) · #(b → j), plus 1 when a = j for the trivial path.

Implementation notes

Quiver.Path recurses on its target vertex, so — unlike the last arrow, which is the head of the Quiver.Path.cons constructor — the first arrow of a path is not visible to a match. The forward map pathFirstArrowSplit is therefore an honest recursion over the path: on p.cons e it splits p and, if p turned out to be trivial, promotes e to the first arrow, transporting it along the equality of vertices with Quiver.Hom.cast; otherwise it appends e to the tail. The inverse pathOfFirstArrow is the direct construction e.toPath.comp p, and the two round trips are inductions over the same recursion. Both maps are private: the four characteristic lemmas TauCeti.pathFirstArrowEquiv_nil, TauCeti.pathFirstArrowEquiv_toPath_comp, TauCeti.pathFirstArrowEquiv_symm_inl and TauCeti.pathFirstArrowEquiv_symm_inr are the whole public interface, and consumers never unfold the equivalence.

The proposition a = j is wrapped in PLift only to make the summand a type, so that Nat.card applies, exactly as in the last-arrow decomposition.

References

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

theorem TauCeti.exists_hom_mem_path_vertices_of_mem_dropLast {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) {u : V} : u ∈ p.vertices.dropLast → ∃ w ∈ p.vertices, Nonempty (u ⟶ w)

Every occurrence in a path's vertex list except the final one is the source of an arrow to another vertex visited by the path. The final entry of the vertex list is the occurrence removed by List.dropLast; the endpoint vertex may still occur earlier.

theorem TauCeti.exists_hom_mem_path_vertices {V : Type u} [Quiver V] {a : V} (p : Quiver.Path a a) (hp : p ≠ Quiver.Path.nil) {u : V} (hu : u ∈ p.vertices) : ∃ w ∈ p.vertices, Nonempty (u ⟶ w)

Every vertex of a closed path of positive length is the source of an arrow to another vertex visited by the path. List.dropLast removes the final endpoint occurrence. On a nontrivial closed path the same vertex also occurs initially, so it remains in List.dropLast and the preceding result applies.

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

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

Equations

• TauCeti.pathFirstArrowEquiv a j = { toFun := TauCeti.pathFirstArrowSplit✝, invFun := TauCeti.pathOfFirstArrow✝, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.pathFirstArrowEquiv_nil {V : Type u} [Quiver V] (a : V) : (pathFirstArrowEquiv a a) Quiver.Path.nil = Sum.inl { down := ⋯ }

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

@[simp]

theorem TauCeti.pathFirstArrowEquiv_toPath_comp {V : Type u} [Quiver V] {a b j : V} (e : a ⟶ b) (q : Quiver.Path b j) : (pathFirstArrowEquiv a j) (e.toPath.comp q) = Sum.inr ⟨b, (e, q)⟩

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

@[simp]

theorem TauCeti.pathFirstArrowEquiv_symm_inl {V : Type u} [Quiver V] (a : V) : (pathFirstArrowEquiv a a).symm (Sum.inl { down := ⋯ }) = Quiver.Path.nil

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

@[simp]

theorem TauCeti.pathFirstArrowEquiv_symm_inr {V : Type u} [Quiver V] {a j : V} (b : V) (e : a ⟶ b) (q : Quiver.Path b j) : (pathFirstArrowEquiv a j).symm (Sum.inr ⟨b, (e, q)⟩) = e.toPath.comp q

The right summand of the first-arrow decomposition recomposes by prepending the first arrow.

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

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

This is the mirror image of TauCeti.card_path_eq_ite_add_sum_lastArrow.