The basis of a path algebra truncated by path length

The quotient of a path algebra by the span of paths of length at least n has precisely the shorter paths as a basis. When the vertex type is finite, this gives a concrete basis for the quotient by the nth power of the arrow ideal. It is useful for calculations with bound quivers, including the radical-square-zero presentation of the preprojective algebra of A₂. The paths of length less than two are the trivial paths and the arrows (TauCeti.shortPathTwoEquiv), so the quotient by the square of the arrow ideal has the vertices and the arrows as a basis.

The construction follows the path-basis description of truncated quiver algebras in Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter II.

@[reducible, inline]

abbrev TauCeti.ShortPath (Q : Type u) [Quiver Q] (n : ℕ) : Type (max 0 u v)

Paths of length strictly less than n.

noncomputable def TauCeti.shortPathCoords (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : pathAlgebra k Q →ₗ[k] ShortPath Q n →₀ k

The coordinates of a path-algebra element on paths shorter than n.

@[simp]

theorem TauCeti.shortPathCoords_apply (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) (x : pathAlgebra k Q) (p : ShortPath Q n) : ((shortPathCoords k Q n) x) p = ((pathAlgebraBasis k Q).repr x) ↑p

Reading the coordinate of a short path agrees with the path-basis coordinate.

theorem TauCeti.ker_shortPathCoords (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : (shortPathCoords k Q n).ker = pathSpan k Q n

The coordinate map kills exactly the span of paths of length at least n.

theorem TauCeti.shortPathCoords_surjective (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : Function.Surjective ⇑(shortPathCoords k Q n)

Every collection of coefficients on short paths extends to a path-algebra element.

def TauCeti.shortPathTwoEquiv {Q : Type u} [Quiver Q] : Q ⊕ (i : Q) × (j : Q) × (i ⟶ j) ≃ ShortPath Q 2

The paths of length less than two are the trivial paths at the vertices and the length-one paths of the arrows.

@[simp]

theorem TauCeti.coe_shortPathTwoEquiv_inl {Q : Type u} [Quiver Q] (i : Q) : ↑(shortPathTwoEquiv (Sum.inl i)) = ⟨i, ⟨i, Quiver.Path.nil⟩⟩

A vertex corresponds to its trivial path.

@[simp]

theorem TauCeti.coe_shortPathTwoEquiv_inr {Q : Type u} [Quiver Q] (a : (i : Q) × (j : Q) × (i ⟶ j)) : ↑(shortPathTwoEquiv (Sum.inr a)) = ⟨a.fst, ⟨a.snd.fst, a.snd.snd.toPath⟩⟩

An arrow corresponds to its length-one path.

noncomputable def TauCeti.truncatedPathEquiv (k : Type w) (Q : Type u) [Ring k] [Quiver Q] (n : ℕ) : (pathAlgebra k Q ⧸ pathSpan k Q n) ≃ₗ[k] ShortPath Q n →₀ k

The quotient by the length filtration is the free module on short paths.

@[simp]

theorem TauCeti.truncatedPathEquiv_mk (k : Type w) (Q : Type u) [Ring k] [Quiver Q] (n : ℕ) (x : pathAlgebra k Q) : (truncatedPathEquiv k Q n) (Submodule.Quotient.mk x) = (shortPathCoords k Q n) x

The equivalence reads the short-path coordinates of a quotient representative.

noncomputable def TauCeti.arrowIdealQuotientEquiv (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (n : ℕ) : (pathAlgebra k Q ⧸ arrowIdeal k Q ^ n) ≃ₗ[k] ShortPath Q n →₀ k

The quotient by an arrow-ideal power is linearly equivalent to the free module on paths shorter than that power.

@[simp]

theorem TauCeti.arrowIdealQuotientEquiv_mk (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (n : ℕ) (x : pathAlgebra k Q) : (arrowIdealQuotientEquiv k Q n) ((Ideal.Quotient.mk (arrowIdeal k Q ^ n)) x) = (shortPathCoords k Q n) x

The quotient equivalence reads the coefficients of every short path.

noncomputable def TauCeti.arrowIdealQuotientBasis (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (n : ℕ) : Module.Basis (ShortPath Q n) k (pathAlgebra k Q ⧸ arrowIdeal k Q ^ n)

The classes of paths shorter than n form a basis of the quotient by R^n, where R is the arrow ideal.

@[simp]

theorem TauCeti.arrowIdealQuotientBasis_apply (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (n : ℕ) (p : ShortPath Q n) : (arrowIdealQuotientBasis k Q n) p = (Ideal.Quotient.mk (arrowIdeal k Q ^ n)) (PathAlgebra.ofPath ↑p)

A short path's basis vector is its class in the quotient by R^n.

@[simp]

theorem TauCeti.arrowIdealQuotientBasis_repr (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (n : ℕ) (x : pathAlgebra k Q ⧸ arrowIdeal k Q ^ n) : (arrowIdealQuotientBasis k Q n).repr x = (arrowIdealQuotientEquiv k Q n) x

The short-path basis coordinates are exactly the restricted path coordinates.

theorem TauCeti.finrank_arrowIdealQuotient (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] [Nontrivial k] (n : ℕ) : Module.finrank k (pathAlgebra k Q ⧸ arrowIdeal k Q ^ n) = Nat.card (ShortPath Q n)

The finrank of a truncated path algebra is Nat.card of its short paths. When the quiver has finitely many arrows between any two vertices this is the dimension and the number of short paths; otherwise both sides may be infinite and hence both equal 0.

instance TauCeti.instFiniteShortPath (Q : Type u) [Quiver Q] [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] (n : ℕ) : Finite (ShortPath Q n)

A finite quiver has finitely many paths below any fixed length.

instance TauCeti.instFiniteQuotientPathAlgebraIdealHPowNatArrowIdeal (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] (n : ℕ) : Module.Finite k (pathAlgebra k Q ⧸ arrowIdeal k Q ^ n)

A quotient by an arrow-ideal power is a finite module for a finite quiver.