Path algebras of quivers

The path algebra kQ of a quiver Q over a semiring k is the free k-module on the paths of Q, with the product of two paths their concatenation when they are composable and 0 otherwise.

The path index TauCeti.Quiver.TotalPath and its partial concatenation are developed in TauCeti.Combinatorics.Quiver.TotalPath, independently of the coefficient semiring.

Paths are concatenated in the later factor first order: for p : Path a b and q : Path c a, the product of the corresponding basis elements is the basis element of q.comp p : Path c b. With this convention an arrow α : i ⟶ j satisfies eⱼ * α = α = α * eᵢ for the vertex idempotents e, so left multiplication by α carries the i-component of a left module to its j-component: representations of Q are left kQ-modules.

Main definitions

• TauCeti.pathAlgebra k Q: the path algebra, with TauCeti.PathAlgebra.single its basis elements. For any quiver it is a non-unital semiring or ring, associative or not, whenever k is, with scalars from k passing through products (on both sides when k is commutative), and it carries Semiring, Ring and Algebra k structures once the vertex type is Finite, finiteness being what makes the unit 1 = ∑ᵥ eᵥ exist.
• TauCeti.PathAlgebra.vertexIdempotent: the idempotent eᵥ given by the trivial path at v.
• TauCeti.pathAlgebraBasis: the paths of Q as a k-basis of kQ.
• TauCeti.PathAlgebra.liftNonUnitalAlgHom: extends a multiplicative assignment on paths to a non-unital algebra homomorphism, for any quiver and a possibly non-associative target.
• TauCeti.PathAlgebra.liftAlgHom: the unital universal property of the path algebra, extending an assignment of elements of a k-algebra to the basis paths to an algebra homomorphism out of kQ, the only one doing so by TauCeti.PathAlgebra.liftAlgHom_unique.

Main results

• TauCeti.PathAlgebra.single_mul_single: the defining product of two basis paths.
• TauCeti.PathAlgebra.one_def: the vertex idempotents sum to 1; they are orthogonal by TauCeti.PathAlgebra.vertexIdempotent_mul_vertexIdempotent_of_ne, idempotent by TauCeti.PathAlgebra.vertexIdempotent_mul_self and nonzero by TauCeti.PathAlgebra.vertexIdempotent_ne_zero. The first three are bundled as TauCeti.PathAlgebra.completeOrthogonalIdempotents_vertexIdempotent.
• TauCeti.module_finite_pathAlgebra and TauCeti.finrank_pathAlgebra: kQ is a free module of rank the number of paths of Q, with TauCeti.pathAlgebraBasis_repr_single reading off the coordinates of a basis path and TauCeti.linearIndependent_ofPath recording that the path basis is linearly independent. Over a nonzero k the finiteness is an equivalence, TauCeti.module_finite_pathAlgebra_iff; the specialization to a finite acyclic quiver, whose paths are finite, is TauCeti.finiteDimensional_pathAlgebra_of_isAcyclic in TauCeti.RepresentationTheory.Quiver.Acyclic.PathAlgebra.
• TauCeti.vertexIdempotent_mul_mul_vertexIdempotent: when the trivial path is the only path from v to itself, eᵥ f eᵥ is the coefficient of f on that path, times eᵥ, so the corner eᵥ kQ eᵥ is a copy of k. This is what makes the trivial paths visible to a two-sided ideal.
• TauCeti.PathAlgebra.adjoin_vertexIdempotents_union_arrows: the vertex idempotents and arrows generate the path algebra.

Implementation notes

pathAlgebra k Q is a semireducible type synonym for Quiver.TotalPath Q →₀ k, following the pattern of MonoidAlgebra: were it reducible, instance search would unfold it and pick up the pointwise multiplication of Finsupp. The multiplication is therefore introduced as an operation mul' on Quiver.TotalPath Q →₀ k (with singleOption naming the product of two basis paths, which is a basis path or 0), where the Finsupp API applies without friction; the ring axioms are proved there and transferred definitionally.

That whole layer is private. The exposed Mul instance spells out the same operation because it cannot mention a private declaration; mul_def records their definitional agreement. The ring axioms reach the structure instances through a by exact for the same reason. pathAlgebra is the only definition whose body is @[expose]d, because the transported instances unfold it; every other definition here is opaque downstream, which sees the path algebra through its algebraic structure and the lemmas below (ofPath_eq_single and vertexIdempotent_eq_single for the basis elements, single_mul_single and the mul? lemmas for products) rather than through the Finsupp representation.

Since Finset.univ is data, the unit is the sum of the vertex idempotents over a Fintype structure chosen internally by Fintype.ofFinite; the unital instances therefore ask only for [Finite Q], and one_def identifies 1 with the sum over any Fintype Q a caller supplies.

References

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

The path algebra

def TauCeti.pathAlgebra (k : Type w) (Q : Type u) [Zero k] [Quiver Q] : Type (max w v u)

The path algebra of a quiver Q over k: the free k-module on the paths of Q, with multiplication the concatenation of composable paths in the later factor first order, and 0 on non-composable pairs.

This is a semireducible type synonym so that instance search does not confuse the path multiplication with the pointwise multiplication of Finsupp.

Equations

• TauCeti.pathAlgebra k Q = (TauCeti.Quiver.TotalPath Q →₀ k)

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instAddCommMonoidPathAlgebra {k : Type w} {Q : Type u} [AddCommMonoid k] [Quiver Q] : AddCommMonoid (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instInhabitedPathAlgebra {k : Type w} {Q : Type u} [AddCommMonoid k] [Quiver Q] : Inhabited (pathAlgebra k Q)

Equations

• TauCeti.PathAlgebra.instInhabitedPathAlgebra = { default := TauCeti.PathAlgebra.instInhabitedPathAlgebra._aux_1 }

noncomputable def TauCeti.PathAlgebra.single {k : Type w} {Q : Type u} [AddCommMonoid k] [Quiver Q] (x : Quiver.TotalPath Q) (c : k) : pathAlgebra k Q

The basis element of the path algebra attached to a path, with a coefficient.

Equations

• TauCeti.PathAlgebra.single x c = Finsupp.single x c

@[simp]

theorem TauCeti.PathAlgebra.single_zero {k : Type w} {Q : Type u} [AddCommMonoid k] [Quiver Q] (x : Quiver.TotalPath Q) : single x 0 = 0

A basis path with coefficient zero is zero.

theorem TauCeti.PathAlgebra.single_add {k : Type w} {Q : Type u} [AddCommMonoid k] [Quiver Q] (x : Quiver.TotalPath Q) (c d : k) : single x (c + d) = single x c + single x d

Basis paths are additive in their coefficient.

theorem TauCeti.PathAlgebra.induction_linear {k : Type w} {Q : Type u} [AddCommMonoid k] [Quiver Q] {motive : pathAlgebra k Q → Prop} (f : pathAlgebra k Q) (zero : motive 0) (add : ∀ (f g : pathAlgebra k Q), motive f → motive g → motive (f + g)) (single : ∀ (x : Quiver.TotalPath Q) (c : k), motive (single x c)) : motive f

Additive induction on the path algebra: it suffices to treat 0, sums, and basis paths.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instModulePathAlgebra {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] : Module k (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PathAlgebra.smul_single {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (r : k) (x : Quiver.TotalPath Q) (c : k) : r • single x c = single x (r * c)

Scaling a basis path scales its coefficient.

The multiplication

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instMulPathAlgebra {k : Type w} {Q : Type u} [NonUnitalNonAssocSemiring k] [Quiver Q] : Mul (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instNonUnitalNonAssocSemiringPathAlgebra {k : Type w} {Q : Type u} [NonUnitalNonAssocSemiring k] [Quiver Q] : NonUnitalNonAssocSemiring (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

Products of basis paths

@[simp]

theorem TauCeti.PathAlgebra.single_mul_single {k : Type w} {Q : Type u} [NonUnitalNonAssocSemiring k] [Quiver Q] (x y : Quiver.TotalPath Q) (a b : k) : single x a * single y b = (x.mul? y).elim 0 fun (z : Quiver.TotalPath Q) => single z (a * b)

The defining product of two basis paths: their concatenation, later factor first, when they are composable, and 0 otherwise.

theorem TauCeti.PathAlgebra.single_mul_single_of_comp {k : Type w} {Q : Type u} [NonUnitalNonAssocSemiring k] [Quiver Q] {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a) (r s : k) : single ⟨a, ⟨b, p⟩⟩ r * single ⟨c, ⟨a, q⟩⟩ s = single ⟨c, ⟨b, q.comp p⟩⟩ (r * s)

Multiplying two composable basis paths concatenates them, later factor first.

theorem TauCeti.PathAlgebra.single_mul_single_of_not_composable {k : Type w} {Q : Type u} [NonUnitalNonAssocSemiring k] [Quiver Q] {x y : Quiver.TotalPath Q} (h : y.snd.fst ≠ x.fst) (r s : k) : single x r * single y s = 0

The product of two basis paths that are not composable vanishes.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instNonUnitalSemiringPathAlgebra {k : Type w} {Q : Type u} [NonUnitalSemiring k] [Quiver Q] : NonUnitalSemiring (pathAlgebra k Q)

Equations

• TauCeti.PathAlgebra.instNonUnitalSemiringPathAlgebra = { toNonUnitalNonAssocSemiring := TauCeti.PathAlgebra.instNonUnitalNonAssocSemiringPathAlgebra, mul_assoc := ⋯ }

instance TauCeti.PathAlgebra.instIsScalarTowerPathAlgebra {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] : IsScalarTower k (pathAlgebra k Q) (pathAlgebra k Q)

noncomputable def TauCeti.PathAlgebra.ofPath {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x : Quiver.TotalPath Q) : pathAlgebra k Q

The basis element of the path algebra attached to a path.

Equations

• TauCeti.PathAlgebra.ofPath x = TauCeti.PathAlgebra.single x 1

theorem TauCeti.PathAlgebra.ofPath_eq_single {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x : Quiver.TotalPath Q) : ofPath x = single x 1

A path is the basis element it indexes, with coefficient one.

theorem TauCeti.PathAlgebra.single_eq_smul_ofPath {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x : Quiver.TotalPath Q) (c : k) : single x c = c • ofPath x

A basis path carrying a coefficient is that coefficient acting on the basis element.

theorem TauCeti.PathAlgebra.ofPath_mul_ofPath {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x y : Quiver.TotalPath Q) : ofPath x * ofPath y = (x.mul? y).elim 0 fun (z : Quiver.TotalPath Q) => ofPath z

The defining product of two basis paths: their concatenation, later factor first, when they are composable, and 0 otherwise. This is TauCeti.PathAlgebra.single_mul_single read on the path basis.

@[simp]

theorem TauCeti.PathAlgebra.ofPath_mul_ofPath_of_comp {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a) : ofPath ⟨a, ⟨b, p⟩⟩ * ofPath ⟨c, ⟨a, q⟩⟩ = ofPath ⟨c, ⟨b, q.comp p⟩⟩

Two composable paths multiply to their concatenation, later factor first.

@[simp]

theorem TauCeti.PathAlgebra.ofPath_mul_ofPath_of_not_composable {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {x y : Quiver.TotalPath Q} (h : y.snd.fst ≠ x.fst) : ofPath x * ofPath y = 0

Two paths that do not meet multiply to zero.

The vertex idempotents

noncomputable def TauCeti.PathAlgebra.vertexIdempotent (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : pathAlgebra k Q

The idempotent of the path algebra attached to a vertex: the trivial path at that vertex.

Equations

• TauCeti.PathAlgebra.vertexIdempotent k v = TauCeti.PathAlgebra.ofPath ⟨v, ⟨v, Quiver.Path.nil⟩⟩

theorem TauCeti.PathAlgebra.vertexIdempotent_eq_single {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : vertexIdempotent k v = single ⟨v, ⟨v, Quiver.Path.nil⟩⟩ 1

The vertex idempotent is the basis element of the trivial path, with coefficient one.

theorem TauCeti.PathAlgebra.vertexIdempotent_eq_ofPath (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : vertexIdempotent k v = ofPath ⟨v, ⟨v, Quiver.Path.nil⟩⟩

The vertex idempotent is the basis element of the trivial path at its vertex.

@[simp]

theorem TauCeti.PathAlgebra.vertexIdempotent_mul_single {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x : Quiver.TotalPath Q) (r : k) : vertexIdempotent k x.snd.fst * single x r = single x r

The vertex idempotent at the target of a path is a left unit for it.

@[simp]

theorem TauCeti.PathAlgebra.single_mul_vertexIdempotent {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x : Quiver.TotalPath Q) (r : k) : single x r * vertexIdempotent k x.fst = single x r

The vertex idempotent at the source of a path is a right unit for it.

@[simp]

theorem TauCeti.PathAlgebra.vertexIdempotent_mul_ofPath {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b : Q} (p : Quiver.Path a b) : vertexIdempotent k b * ofPath ⟨a, ⟨b, p⟩⟩ = ofPath ⟨a, ⟨b, p⟩⟩

The vertex idempotent at the target of a path is a left unit for its canonical element.

@[simp]

theorem TauCeti.PathAlgebra.ofPath_mul_vertexIdempotent {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b : Q} (p : Quiver.Path a b) : ofPath ⟨a, ⟨b, p⟩⟩ * vertexIdempotent k a = ofPath ⟨a, ⟨b, p⟩⟩

The vertex idempotent at the source of a path is a right unit for its canonical element.

@[simp]

theorem TauCeti.PathAlgebra.vertexIdempotent_mul_ofPath_of_ne {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {v : Q} (x : Quiver.TotalPath Q) (h : v ≠ x.snd.fst) : vertexIdempotent k v * ofPath x = 0

A vertex idempotent not at the target of a path annihilates its canonical element on the left.

@[simp]

theorem TauCeti.PathAlgebra.ofPath_mul_vertexIdempotent_of_ne {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {v : Q} (x : Quiver.TotalPath Q) (h : v ≠ x.fst) : ofPath x * vertexIdempotent k v = 0

A vertex idempotent not at the source of a path annihilates its canonical element on the right.

@[simp]

theorem TauCeti.PathAlgebra.vertexIdempotent_mul_vertexIdempotent_of_ne {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {u v : Q} (h : u ≠ v) : vertexIdempotent k u * vertexIdempotent k v = 0

Distinct vertex idempotents are orthogonal.

@[simp]

theorem TauCeti.PathAlgebra.vertexIdempotent_mul_self {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : vertexIdempotent k v * vertexIdempotent k v = vertexIdempotent k v

The vertex idempotents are idempotent.

@[simp]

theorem TauCeti.PathAlgebra.vertexIdempotent_ne_zero {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [Nontrivial k] (v : Q) : vertexIdempotent k v ≠ 0

Over a nonzero base ring, a vertex idempotent is nonzero.

The unit

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instOnePathAlgebra {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [Finite Q] : One (pathAlgebra k Q)

Equations

• TauCeti.PathAlgebra.instOnePathAlgebra = { one := ∑ v : Q, TauCeti.PathAlgebra.vertexIdempotent k v }

theorem TauCeti.PathAlgebra.one_def {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [Finite Q] [Fintype Q] : 1 = ∑ v : Q, vertexIdempotent k v

The unit of the path algebra is the sum of the vertex idempotents: the vertex idempotents are a decomposition of the unit.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instSemiringPathAlgebra {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [Finite Q] : Semiring (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.PathAlgebra.completeOrthogonalIdempotents_vertexIdempotent (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] [Finite Q] [Fintype Q] : CompleteOrthogonalIdempotents fun (v : Q) => vertexIdempotent k v

The vertex idempotents are a complete orthogonal family of idempotents: they are idempotent, pairwise orthogonal, and sum to 1. This bundles TauCeti.PathAlgebra.one_def with the orthogonality and idempotency above.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instAddCommGroupPathAlgebra {k : Type w} {Q : Type u} [Quiver Q] [AddCommGroup k] : AddCommGroup (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instNonUnitalNonAssocRingPathAlgebra {k : Type w} {Q : Type u} [Quiver Q] [NonUnitalNonAssocRing k] : NonUnitalNonAssocRing (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instNonUnitalRingPathAlgebra {k : Type w} {Q : Type u} [Quiver Q] [NonUnitalRing k] : NonUnitalRing (pathAlgebra k Q)

Equations

• TauCeti.PathAlgebra.instNonUnitalRingPathAlgebra = { toNonUnitalNonAssocRing := TauCeti.PathAlgebra.instNonUnitalNonAssocRingPathAlgebra, mul_assoc := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instRingPathAlgebraOfFinite {k : Type w} {Q : Type u} [Quiver Q] [Ring k] [Finite Q] : Ring (pathAlgebra k Q)

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.PathAlgebra.instSMulCommClassPathAlgebra {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] : SMulCommClass k (pathAlgebra k Q) (pathAlgebra k Q)

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.instAlgebraPathAlgebra {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : Algebra k (pathAlgebra k Q)

Equations

• TauCeti.PathAlgebra.instAlgebraPathAlgebra = Algebra.ofModule ⋯ ⋯

theorem TauCeti.PathAlgebra.algebraMap_apply {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] [Fintype Q] (r : k) : (algebraMap k (pathAlgebra k Q)) r = ∑ v : Q, r • vertexIdempotent k v

The image of a scalar in the path algebra spreads it over the vertex idempotents.

The path basis

noncomputable def TauCeti.pathAlgebraBasis (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] : Module.Basis (Quiver.TotalPath Q) k (pathAlgebra k Q)

The paths of Q are a k-basis of the path algebra.

Equations

• TauCeti.pathAlgebraBasis k Q = Finsupp.basisSingleOne

@[simp]

theorem TauCeti.coe_pathAlgebraBasis (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] : ⇑(pathAlgebraBasis k Q) = fun (x : Quiver.TotalPath Q) => PathAlgebra.ofPath x

The path basis consists of the basis paths.

theorem TauCeti.module_finite_pathAlgebra (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] [Finite (Quiver.TotalPath Q)] : Module.Finite k (pathAlgebra k Q)

The path algebra of a quiver with finitely many paths is a finite k-module.

theorem TauCeti.module_finite_pathAlgebra_iff (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] [Nontrivial k] : Module.Finite k (pathAlgebra k Q) ↔ Finite (Quiver.TotalPath Q)

The path algebra is a finite module exactly when the quiver has finitely many paths, over a nonzero base ring. Over the zero ring the path algebra is the zero module however many paths Q has.

theorem TauCeti.linearIndependent_ofPath (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] : LinearIndependent k PathAlgebra.ofPath

The paths form a linearly independent family in the path algebra.

@[simp]

theorem TauCeti.pathAlgebraBasis_repr_single {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x : Quiver.TotalPath Q) (c : k) : (pathAlgebraBasis k Q).repr (PathAlgebra.single x c) = Finsupp.single x c

The coordinates of a basis path for the path basis.

@[simp]

theorem TauCeti.pathAlgebraBasis_repr_vertexIdempotent_mul {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [DecidableEq Q] (v : Q) (f : pathAlgebra k Q) (x : Quiver.TotalPath Q) : ((pathAlgebraBasis k Q).repr (PathAlgebra.vertexIdempotent k v * f)) x = if x.snd.fst = v then ((pathAlgebraBasis k Q).repr f) x else 0

The coordinates of eᵥ f: left multiplication by the vertex idempotent at v keeps the coordinates of f on the paths ending at v and kills the others.

theorem TauCeti.vertexIdempotent_mul_mul_vertexIdempotent {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (v : Q) (h : ∀ (p : Quiver.Path v v), p = Quiver.Path.nil) (f : pathAlgebra k Q) : PathAlgebra.vertexIdempotent k v * f * PathAlgebra.vertexIdempotent k v = ((pathAlgebraBasis k Q).repr f) ⟨v, ⟨v, Quiver.Path.nil⟩⟩ • PathAlgebra.vertexIdempotent k v

Multiplying on both sides by a vertex idempotent reads off a coordinate. When the trivial path is the only path from v to itself, eᵥ f eᵥ is the coordinate of f on that path, times eᵥ, so that the corner eᵥ kQ eᵥ is a copy of k. An acyclic quiver supplies the hypothesis through TauCeti.Quiver.IsAcyclic.eq_nil.

The universal property

noncomputable def TauCeti.PathAlgebra.liftLinear (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [AddCommMonoid B] [Module k B] (F : Quiver.TotalPath Q → B) : pathAlgebra k Q →ₗ[k] B

The k-linear map extending an assignment of module elements to the basis paths. Its multiplicative upgrade TauCeti.PathAlgebra.liftNonUnitalAlgHom is available when the assignment concatenates composable paths and annihilates products of paths that do not meet. For finite vertex types, TauCeti.PathAlgebra.liftAlgHom also preserves the unit when the trivial paths map to a decomposition of the target unit.

Equations

• TauCeti.PathAlgebra.liftLinear k F = ((TauCeti.pathAlgebraBasis k Q).constr ℕ) F

@[simp]

theorem TauCeti.PathAlgebra.liftLinear_ofPath (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [AddCommMonoid B] [Module k B] (F : Quiver.TotalPath Q → B) (x : Quiver.TotalPath Q) : (liftLinear k F) (ofPath x) = F x

The linear extension of an assignment agrees with it on the basis paths.

@[simp]

theorem TauCeti.PathAlgebra.liftLinear_single (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [AddCommMonoid B] [Module k B] (F : Quiver.TotalPath Q → B) (x : Quiver.TotalPath Q) (c : k) : (liftLinear k F) (single x c) = c • F x

The linear extension of an assignment on a basis path with a coefficient.

@[simp]

theorem TauCeti.PathAlgebra.liftLinear_one (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [AddCommMonoidWithOne B] [Module k B] (F : Quiver.TotalPath Q → B) [Finite Q] (hone : ∑ v : Q, F ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 1) : (liftLinear k F) 1 = 1

The linear extension of an assignment sending the trivial paths to a decomposition of 1 preserves the unit.

theorem TauCeti.PathAlgebra.nonUnitalAlgHom_ext (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [DistribMulAction k B] ⦃f g : pathAlgebra k Q →ₙₐ[k] B⦄ (h : ∀ (x : Quiver.TotalPath Q), f (ofPath x) = g (ofPath x)) : f = g

Non-unital algebra homomorphisms out of a path algebra are determined by their values on the basis paths.

theorem TauCeti.PathAlgebra.nonUnitalAlgHom_ext_iff {k : Type w} {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [DistribMulAction k B] {f g : pathAlgebra k Q →ₙₐ[k] B} : f = g ↔ ∀ (x : Quiver.TotalPath Q), f (ofPath x) = g (ofPath x)

theorem TauCeti.PathAlgebra.liftLinear_mul (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [Module k B] [IsScalarTower k B B] [SMulCommClass k B B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) (f g : pathAlgebra k Q) : (liftLinear k F) (f * g) = (liftLinear k F) f * (liftLinear k F) g

A path assignment respecting concatenation and vanishing on noncomposable products has a multiplicative linear extension. No finiteness assumption on the vertex type or unit in the target is required.

noncomputable def TauCeti.PathAlgebra.liftNonUnitalAlgHom (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [Module k B] [IsScalarTower k B B] [SMulCommClass k B B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) : pathAlgebra k Q →ₙₐ[k] B

Extend a path assignment respecting concatenation and vanishing on noncomposable products to a non-unital algebra homomorphism. This is the path-algebra analogue of MonoidAlgebra.liftMagma: the quiver may have infinitely many vertices, and the target need not have a unit or associative multiplication.

Equations

• TauCeti.PathAlgebra.liftNonUnitalAlgHom k F hcomp hzero = { toFun := (↑(TauCeti.PathAlgebra.liftLinear k F).toAddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.PathAlgebra.coe_liftNonUnitalAlgHom (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [Module k B] [IsScalarTower k B B] [SMulCommClass k B B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) : ⇑(liftNonUnitalAlgHom k F ⋯ ⋯) = ⇑(liftLinear k F)

The non-unital lift has the given linear extension as its underlying function.

@[simp]

theorem TauCeti.PathAlgebra.liftNonUnitalAlgHom_ofPath (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [Module k B] [IsScalarTower k B B] [SMulCommClass k B B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) (x : Quiver.TotalPath Q) : (liftNonUnitalAlgHom k F ⋯ ⋯) (ofPath x) = F x

The non-unital lift agrees with the assignment on basis paths.

@[simp]

theorem TauCeti.PathAlgebra.liftNonUnitalAlgHom_single (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [Module k B] [IsScalarTower k B B] [SMulCommClass k B B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) (x : Quiver.TotalPath Q) (c : k) : (liftNonUnitalAlgHom k F ⋯ ⋯) (single x c) = c • F x

The non-unital lift sends a scaled basis path to the scaled assigned value.

theorem TauCeti.PathAlgebra.liftNonUnitalAlgHom_unique (k : Type w) {Q : Type u} {B : Type u_1} [Semiring k] [Quiver Q] [NonUnitalNonAssocSemiring B] [Module k B] [IsScalarTower k B B] [SMulCommClass k B B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) (G : pathAlgebra k Q →ₙₐ[k] B) (hG : ∀ (x : Quiver.TotalPath Q), G (ofPath x) = F x) : G = liftNonUnitalAlgHom k F ⋯ ⋯

The non-unital lift is the unique non-unital algebra homomorphism extending the assignment.

noncomputable def TauCeti.PathAlgebra.liftAlgHom (k : Type w) {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) [Finite Q] (hone : ∑ v : Q, F ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 1) : pathAlgebra k Q →ₐ[k] B

The universal property of the path algebra: an assignment F of elements of a k-algebra B to the basis paths extends to a k-algebra homomorphism kQ →ₐ[k] B as soon as it turns the three defining products of kQ into products in B — composable paths concatenate (hcomp, later factor first, as TauCeti.PathAlgebra.single_mul_single_of_comp multiplies them), paths that do not meet annihilate one another (hzero), and the trivial paths give a decomposition of the unit (hone), as TauCeti.PathAlgebra.one_def says of the vertex idempotents.

Equations

• TauCeti.PathAlgebra.liftAlgHom k F hcomp hzero hone = AlgHom.ofLinearMap (TauCeti.PathAlgebra.liftLinear k F) ⋯ ⋯

@[simp]

theorem TauCeti.PathAlgebra.liftAlgHom_ofPath (k : Type w) {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) [Finite Q] (hone : ∑ v : Q, F ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 1) (x : Quiver.TotalPath Q) : (liftAlgHom k F ⋯ ⋯ hone) (ofPath x) = F x

The lift extends the assignment: a basis path goes to the element it was assigned.

@[simp]

theorem TauCeti.PathAlgebra.coe_liftAlgHom (k : Type w) {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) [Finite Q] (hone : ∑ v : Q, F ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 1) : NonUnitalAlgHomClass.toNonUnitalAlgHom (liftAlgHom k F ⋯ ⋯ hone) = liftNonUnitalAlgHom k F ⋯ ⋯

Forgetting the unit condition on the unital lift gives the non-unital lift.

@[simp]

theorem TauCeti.PathAlgebra.liftAlgHom_single (k : Type w) {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) [Finite Q] (hone : ∑ v : Q, F ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 1) (x : Quiver.TotalPath Q) (c : k) : (liftAlgHom k F ⋯ ⋯ hone) (single x c) = c • F x

The lift is k-linear, so a scaled basis path scales the element it was assigned.

theorem TauCeti.PathAlgebra.algHom_ext (k : Type w) {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] [Finite Q] ⦃f g : pathAlgebra k Q →ₐ[k] B⦄ (h : ∀ (x : Quiver.TotalPath Q), f (ofPath x) = g (ofPath x)) : f = g

Algebra homomorphisms out of a path algebra are determined by their values on the paths. This is TauCeti.PathAlgebra.liftAlgHom_unique in the form which compares two given homomorphisms, with no assignment F to name.

theorem TauCeti.PathAlgebra.algHom_ext_iff {k : Type w} {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] [Finite Q] {f g : pathAlgebra k Q →ₐ[k] B} : f = g ↔ ∀ (x : Quiver.TotalPath Q), f (ofPath x) = g (ofPath x)

theorem TauCeti.PathAlgebra.liftAlgHom_unique (k : Type w) {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] (F : Quiver.TotalPath Q → B) (hcomp : ∀ {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a), F ⟨a, ⟨b, p⟩⟩ * F ⟨c, ⟨a, q⟩⟩ = F ⟨c, ⟨b, q.comp p⟩⟩) (hzero : ∀ {x y : Quiver.TotalPath Q}, y.snd.fst ≠ x.fst → F x * F y = 0) [Finite Q] (hone : ∑ v : Q, F ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 1) (G : pathAlgebra k Q →ₐ[k] B) (hG : ∀ (x : Quiver.TotalPath Q), G (ofPath x) = F x) : G = liftAlgHom k F ⋯ ⋯ hone

The lift is the only one: an algebra homomorphism out of kQ taking the value F x on each basis path is TauCeti.PathAlgebra.liftAlgHom.

theorem TauCeti.PathAlgebra.algEquiv_ext (k : Type w) {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] [Finite Q] ⦃f g : pathAlgebra k Q ≃ₐ[k] B⦄ (h : ∀ (x : Quiver.TotalPath Q), f (ofPath x) = g (ofPath x)) : f = g

Algebra isomorphisms out of a path algebra are determined by their values on the paths.

theorem TauCeti.PathAlgebra.algEquiv_ext_iff {k : Type w} {Q : Type u} {B : Type u_1} [CommSemiring k] [Quiver Q] [Semiring B] [Algebra k B] [Finite Q] {f g : pathAlgebra k Q ≃ₐ[k] B} : f = g ↔ ∀ (x : Quiver.TotalPath Q), f (ofPath x) = g (ofPath x)

theorem TauCeti.PathAlgebra.ringHom_ext_of_surjective {k : Type w} {Q : Type u} {A : Type u_1} {B : Type u_2} [CommSemiring k] [Quiver Q] [Finite Q] [Semiring A] [Algebra k A] [NonAssocSemiring B] (q : pathAlgebra k Q →ₐ[k] A) (hq : Function.Surjective ⇑q) {g h : A →+* B} (hscalar : ∀ (r : k), g ((algebraMap k A) r) = h ((algebraMap k A) r)) (hpath : ∀ (x : Quiver.TotalPath Q), g (q (ofPath x)) = h (q (ofPath x))) : g = h

Two ring homomorphisms out of an algebra admitting a surjective map from a path algebra are equal if they agree on coefficients and on the images of all paths.

theorem TauCeti.finrank_pathAlgebra (k : Type w) (Q : Type u) [Semiring k] [StrongRankCondition k] [Quiver Q] : Module.finrank k (pathAlgebra k Q) = Nat.card (Quiver.TotalPath Q)

The finite rank of the path algebra is the number of paths of Q. If there are infinitely many paths, both sides are zero.

noncomputable def TauCeti.PathAlgebra.ofArrow {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b : Q} (e : a ⟶ b) : pathAlgebra k Q

The path-algebra element attached to an arrow.

Equations

• TauCeti.PathAlgebra.ofArrow e = TauCeti.PathAlgebra.ofPath ⟨a, ⟨b, e.toPath⟩⟩

@[simp]

theorem TauCeti.PathAlgebra.ofArrow_eq_ofPath {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b : Q} (e : a ⟶ b) : ofArrow e = ofPath ⟨a, ⟨b, e.toPath⟩⟩

An arrow is the basis element indexed by its length-one path.

theorem TauCeti.PathAlgebra.vertexIdempotent_mul_ofArrow {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [DecidableEq Q] (u : Q) {i j : Q} (b : i ⟶ j) : vertexIdempotent k u * ofArrow b = if j = u then ofArrow b else 0

A vertex idempotent keeps an arrow exactly when the vertex is its target.

theorem TauCeti.PathAlgebra.ofArrow_mul_ofPath {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b c : Q} (e : b ⟶ c) (p : Quiver.Path a b) : ofArrow e * ofPath ⟨a, ⟨b, p⟩⟩ = ofPath ⟨a, ⟨c, p.cons e⟩⟩

Extending a path by an arrow. In the later-factor-first convention the new arrow is the left factor, so the product is the path with that arrow consed on.

theorem TauCeti.PathAlgebra.ofArrow_homOfEq {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b a' b' : Q} (f : a ⟶ b) (ha : a = a') (hb : b = b') : ofArrow (Quiver.homOfEq f ha hb) = ofArrow f

Transporting an arrow along equalities of its source and target does not change the basis element it names, the endpoints of a path being recorded in the path itself.

theorem TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofArrow_mul_single {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {i j s : Q} (b : i ⟶ j) (p : Quiver.Path s i) (c : k) (x : Quiver.TotalPath Q) : ((pathAlgebraBasis k Q).repr (ofArrow b * single ⟨s, ⟨i, p⟩⟩ c)) x = (Finsupp.single ⟨s, ⟨j, p.cons b⟩⟩ c) x

The coordinates of an arrow times a basis path: the basis path extended by the arrow. This is not a simp lemma, since TauCeti.PathAlgebra.ofArrow_eq_ofPath rewrites its left-hand side.

@[simp]

theorem TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofPath_toPath_mul_single {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {i j s : Q} (b : i ⟶ j) (p : Quiver.Path s i) (c : k) (x : Quiver.TotalPath Q) : ((pathAlgebraBasis k Q).repr (ofPath ⟨i, ⟨j, b.toPath⟩⟩ * single ⟨s, ⟨i, p⟩⟩ c)) x = (Finsupp.single ⟨s, ⟨j, p.cons b⟩⟩ c) x

The simp-normal form of TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofArrow_mul_single, in which TauCeti.PathAlgebra.ofArrow_eq_ofPath has written the arrow as its length-one path.

theorem TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofArrow_mul_cons {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {i j s : Q} (b : i ⟶ j) (q : Quiver.Path s i) (f : pathAlgebra k Q) : ((pathAlgebraBasis k Q).repr (ofArrow b * f)) ⟨s, ⟨j, q.cons b⟩⟩ = ((pathAlgebraBasis k Q).repr f) ⟨s, ⟨i, q⟩⟩

Reading off a coordinate through the last arrow: the coordinate of b f on the path q followed by b is the coordinate of f on q.

@[simp]

theorem TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofPath_toPath_mul_cons {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {i j s : Q} (b : i ⟶ j) (q : Quiver.Path s i) (f : pathAlgebra k Q) : ((pathAlgebraBasis k Q).repr (ofPath ⟨i, ⟨j, b.toPath⟩⟩ * f)) ⟨s, ⟨j, q.cons b⟩⟩ = ((pathAlgebraBasis k Q).repr f) ⟨s, ⟨i, q⟩⟩

The simp-normal form of TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofArrow_mul_cons, in which TauCeti.PathAlgebra.ofArrow_eq_ofPath has written the arrow as its length-one path.

theorem TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofArrow_mul_cons_of_ne {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {i i' j s : Q} (b : i ⟶ j) (b' : i' ⟶ j) (hb : ⟨i', b'⟩ ≠ ⟨i, b⟩) (q : Quiver.Path s i) (f : pathAlgebra k Q) : ((pathAlgebraBasis k Q).repr (ofArrow b' * f)) ⟨s, ⟨j, q.cons b⟩⟩ = 0

A path ending in the arrow b has coordinate zero in b' f for every other arrow b' with the same target.

@[simp]

theorem TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofPath_toPath_mul_cons_of_ne {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {i i' j s : Q} (b : i ⟶ j) (b' : i' ⟶ j) (hb : ⟨i', b'⟩ ≠ ⟨i, b⟩) (q : Quiver.Path s i) (f : pathAlgebra k Q) : ((pathAlgebraBasis k Q).repr (ofPath ⟨i', ⟨j, b'.toPath⟩⟩ * f)) ⟨s, ⟨j, q.cons b⟩⟩ = 0

The simp-normal form of TauCeti.PathAlgebra.pathAlgebraBasis_repr_ofArrow_mul_cons_of_ne, in which TauCeti.PathAlgebra.ofArrow_eq_ofPath has written the arrow b' as its length-one path.

theorem TauCeti.PathAlgebra.adjoin_vertexIdempotents_union_arrows {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : Algebra.adjoin k (Set.range (vertexIdempotent k) ∪ Set.range fun (e : (a : Q) × (b : Q) × (a ⟶ b)) => ofArrow e.snd.snd) = ⊤

The vertex idempotents and arrows generate the path algebra. Vertex idempotents are necessary: arrows alone do not generate the path algebra of, for example, a discrete multi-vertex quiver.