Powers of a closed path

A closed path p : Quiver.Path a a can be concatenated with itself, so it has powers p.loopPow n, the path that runs around p exactly n times. Their lengths are the multiples n * p.length of the length of p, so a nontrivial closed path has pairwise distinct powers and the type of closed paths at a is infinite.

That last statement is the source of every "an oriented cycle makes something infinite" argument. In TauCeti.RepresentationTheory.Quiver.Acyclic.FinitePaths it is what turns finiteness of the path space into acyclicity, and through the path basis it is what makes the path algebra of a quiver with an oriented cycle infinite-dimensional.

Main definitions

• Quiver.Path.loopPow: the n-th power of a closed path, p concatenated with itself n times; the empty concatenation is Quiver.Path.nil.

Main results

• Quiver.Path.length_loopPow: the n-th power of p has length n * p.length, and Quiver.Path.loopPow_add adds exponents, which is what makes loopPow a power.
• Quiver.Path.loopPow_injective: the powers of a closed path of positive length are pairwise distinct.
• Quiver.Path.infinite_of_ne_nil: a nontrivial closed path forces infinitely many closed paths, and Quiver.Path.eq_nil_of_finite is the contrapositive: at a vertex carrying finitely many closed paths, the trivial path is the only one.

Implementation notes

The powers are stated for a closed path rather than for a general p : Quiver.Path a b, since concatenating p with itself is what needs a = b. They are not packaged as a Monoid structure on Quiver.Path a a: nothing here needs one, and it would put a multiplication on a type whose elements already compose partially, as arbitrary paths.

def Quiver.Path.loopPow {V : Type u} [Quiver V] {a : V} (p : Path a a) : ℕ → Path a a

The n-th power of a closed path: p concatenated with itself n times, with the empty concatenation the trivial path.

Equations

• p.loopPow 0 = Quiver.Path.nil
• p.loopPow n.succ = (p.loopPow n).comp p

@[simp]

theorem Quiver.Path.loopPow_zero {V : Type u} [Quiver V] {a : V} (p : Path a a) : p.loopPow 0 = nil

@[simp]

theorem Quiver.Path.loopPow_succ {V : Type u} [Quiver V] {a : V} (p : Path a a) (n : ℕ) : p.loopPow (n + 1) = (p.loopPow n).comp p

One more turn around p is one more concatenation, the recursion loopPow is defined by.

@[simp]

theorem Quiver.Path.nil_loopPow {V : Type u} [Quiver V] {a : V} (n : ℕ) : nil.loopPow n = nil

Every power of the trivial path is trivial: running around a path of no arrows changes nothing.

@[simp]

theorem Quiver.Path.length_loopPow {V : Type u} [Quiver V] {a : V} (p : Path a a) (n : ℕ) : (p.loopPow n).length = n * p.length

The n-th power of a closed path has length n * p.length: each of the n turns contributes the arrows of p once.

theorem Quiver.Path.loopPow_add {V : Type u} [Quiver V] {a : V} (p : Path a a) (m n : ℕ) : p.loopPow (m + n) = (p.loopPow m).comp (p.loopPow n)

The powers of a closed path add exponents. With Quiver.Path.loopPow_zero this says that n ↦ p.loopPow n is a monoid homomorphism from (ℕ, +) into the closed paths at a under concatenation.

theorem Quiver.Path.loopPow_injective {V : Type u} [Quiver V] {a : V} {p : Path a a} (hp : 0 < p.length) : Function.Injective p.loopPow

The powers of a closed path of positive length are pairwise distinct, because their lengths are the distinct multiples of p.length.

theorem Quiver.Path.infinite_of_ne_nil {V : Type u} [Quiver V] {a : V} {p : Path a a} (hp : p ≠ nil) : Infinite (Path a a)

A nontrivial closed path forces infinitely many closed paths, namely its powers.

theorem Quiver.Path.eq_nil_of_finite {V : Type u} [Quiver V] {a : V} [Finite (Path a a)] (p : Path a a) : p = nil

Finitely many closed paths at a vertex leave only the trivial one, the contrapositive of Quiver.Path.infinite_of_ne_nil.