Path algebra of a quiver

Stream: Is there code for X?

[Bernhard Reinke]

I might be interested in working with the path algebra of a quiver. I know that paths of a quiver are already defined, but I cannot find a definition of the path algebra. I guess it should be possible to define a MonoidWithZero instance on the total type of paths (with 0 adjoined), provided the type underlying the quiver has decidable equality. But I am not sure whether there is already something for the "MonoidWithZero" algebra of a monoid with zero.

Edit: SemigroupWithZerois more appropriate, see discussion below

[Kevin Buzzard]

Can you compose arbitrary paths in a quiver? There's no endpoint requirement? And is 0 not the identity of the monoid? In a monoid with 0 we have 0*x=0, not 0*x=x

[Bernhard Reinke]

The definition of a path algebra that I know is that p*q = 0 if p and q are not composable. The algebra has an identity element if V is finite, it should be the sum of all paths of length 0 (so the sum of the idempotents associated to the vertices of the quiver)

[Kevin Buzzard]

I'm still a bit confused about something. You said at the end that you wanted to take the "monoid with zero algebra of a monoid with zero". What is the latter monoid with zero? I was just saying that paths don't form a monoid with zero.

[Yaël Dillies]

I think Bernhard wants 0 to be an extra element not corresponding to any path

[Yaël Dillies]

This feels related to the isomorphism between the categories of pointed types with point-preserving functions and usual types with partial functions

[Kevin Buzzard]

But adding a zero to the (sigma type of) all paths in a quiver does not make it into a monoid with zero -- what is the 1? I'm just confused about relating the path algebra story (which I think I understand) into "monoid with zero algebra of a monoid with zero"

[Kevin Buzzard]

It seems more accurate to say something like "semiring non-unital algebra associated to some kind of semigroup with zero thing"

[Yaël Dillies]

Kevin Buzzard said:

what is the 1?

Right, that is the issue, I think

[Bernhard Reinke]

Ah, sorry for the confusion, yes, semigroup with zero would be more appropriate

[Yaël Dillies]

I found this which says

Definition: Let kQ be the vector space with basis the set of all paths in Q, and with the following multiplication: if w, w′ are paths, let ww′ be the concatenation of w and w ′ provided the tail of w is the head of w ′ , and the zero vector otherwise, and extend this multiplication bilinearly to kQ.

[Yaël Dillies]

It looks like docs#MonoidAlgebra

[Kevin Buzzard]

Well I am a little concerned about this claim because if you add the zero to the paths first (which you need to do to get the multiplication) then you'll have two zeros in the monoid algebra

[Bernhard Reinke]

I guess then my question would be if there is a variant of MonoidAlgebra for SemigroupWithZero where the zero element of the SemigroupWithZero is quotiented out. Probably one lemma in this direction would be that for a SemigroupWithZero, the subspace generated by the zero element of the semigroup is an ideal of the "MonoidAlgebra" (which is a priori non unital)

[Kevin Buzzard]

Fortunately, a viable approach to two sided ideals of semirings was merged yesterday, but I don't think we have this construction. Seems to me that there are two approaches. Firstly don't add the zero, then you have a partially defined associative multiplication on the paths, and you can define an associative multiplication on the "monoid algebra" this way because this type has a zero and you can define all bad multiplications to be this zero. Or you can add the zero to the paths first and then make the monoid algebra and then identify the two zeros by quotienting out by the two sided ideal. As far as I know we have neither of these constructions in mathlib.

[Junyan Xu]

My recently merged PR allows taking the quotient of a ring by a two-sided ideal. For quotients of semirings you still have to use RingCon. Not every ideal gives a equivalence relation / congruence in the obvious way.
In this case the congruence would just ignore the 0th coordinate.

[Jan Grabowski]

Just to say that a slightly unconventional approach to the definition of path algebra that might be worth thinking about for formalization is that the path algebra of a quiver is the category algebra of the path category of that quiver. Here, category algebra means the following:

Let C be a small category and let R be a ring. The category algebra R[C] is the R-algebra whose underlying R-module is the free module over the set of morphisms of C and with multiplication defined on basis elements by m(q, p) = q ◦ p if defined and =0 otherwise, where p, q are morphisms in C.

Since the group algebra is the category algebra of the associated 1-object groupoid, the notion of a category algebra would be reusable.

[Bernhard Reinke]

I guess if one wants to be more general one can also construct the category ring of a preadditive category

[Kevin Buzzard]

This looks perfect, except that another thing now occurs to me: now you're talking about categories rather than quivers, I guess I'm realising that probably quiver is probably way too general. You can't even compose paths in quiver if the target of the first equals the source of the second, right? So what does "composable" even mean in

The definition of a path algebra that I know is that p*q = 0 if p and q are not composable.

@Bernhard Reinke ? You would surely need at least what Lean calls a docs#CategoryTheory.CategoryStruct (which supplies the data of composition) to make any sense of this multiplication.

So it seems like this is a variant of MonoidAlgebra and should probably follow the pattern of MonoidAlgebra, i.e. don't assume $R$ is a ring or $M$ is monoid when defining $R[M]$, and then assuming more structure on the the inputs gives you more structure on the outputs. In fact one might naively think that one can reuse MonoidAlgebra, but I think this is probably quite risky.

[Kevin Buzzard]

One could define CategoryAlgebra R C for (C : Type*) and [Zero R] as finitely-supported functions C -> R (yet another alias for Finsupp with yet another multiplication) and then if [Add R] you get [Add CategoryAlgebra R C] and if furthermore [Mul R] and CategoryStruct C then you get Mul (CategoryAlgebra R C) etc. Then if Category C and CommSemiring R you get Semiring (CategoryAlgebra R C) etc etc.

[Kevin Buzzard]

But for quivers you'll have nothing more than AddCommGroup (CategoryAlgebra R C) even if Field R, because you can't compose paths in a quiver as far as I can see so you can't multiply anything other than elements of R.

[Junyan Xu]

We know paths in a quiver form a category: CategoryTheory.Paths.categoryPaths

[Junyan Xu]

To compose composable paths it looks like you need to insert some eqToHom though.

[Bernhard Reinke]

Kevin Buzzard said:

This looks perfect, except that another thing now occurs to me: now you're talking about categories rather than quivers, I guess I'm realising that probably quiver is probably way too general. You can't even compose paths in quiver if the target of the first equals the source of the second, right? So what does "composable" even mean in

The definition of a path algebra that I know is that p*q = 0 if p and q are not composable.

I think in more category theoretic terms, the path category of a quiver is the free category over a quiver (every category becomes a quiver by forgetting composition, and the path category is left adjoint to that). So you can compose paths in a quiver as you would expect from a category

[Bernhard Reinke]

There is also Path.comp

[Bernhard Reinke]

Junyan Xu said:

To compose composable paths it looks like you need to insert some eqToHom though.

that is probably the way to go if one wants to do this via categories. For quivers there is also Quiver.Cast but I don't think there is an direct analogue of eqToHom there

[Junyan Xu]

Yes. Quivers doesn't have identity morphisms so eqToHom can't be defined. Here's a construction of the SemigroupWithZero; you probably want to directly construct an Algebra from the Semigroup instead of needlessly adjoining a zero element though.

import Mathlib.Algebra.GroupWithZero.Defs
import Mathlib.Algebra.Group.WithOne.Defs
import Mathlib.CategoryTheory.PathCategory.Basic

open CategoryTheory
universe u
instance {V} [Quiver.{u+1} V] [DecidableEq V] :
    SemigroupWithZero (WithZero (Σ v : Paths V × Paths V, v.1 ⟶ v.2)) where
  mul := fun p q ↦ p.rec 0 fun p ↦ q.rec 0 fun q ↦ if eq : p.1.2 = q.1.1 then
    some ⟨(p.1.1, q.1.2), p.2 ≫ eqToHom eq ≫ q.2⟩ else 0
  mul_assoc := sorry
  zero := 0
  zero_mul _ := rfl
  mul_zero := by rintro ⟨⟩ <;> rfl

[Bernhard Reinke]

So the path algebra of a quiver is then the category algebra of the path category of a quiver, this is less general than the category algebra of any category. What I was saying is that you can go even one step further: if you have a category field (probably semiring is enough) k, you can also consider the "free k-linear category" of it, where you replace every hom set by the free k-module generated by it, and extend composition bilinearly. You should be able to define the category algebra of a k-linear category, and the path algebra of a quiver is then the category algebra of the free k-linear category of the free category of the quiver.

[Junyan Xu]

I agree we should do things in that generality. (I'm mostly writing this as a demo to show Kevin.) It's less clear whether we want to refactor the existing MonoidAlgebra because defeq is worse. (To keep the current generality, we could define multiplication assuming only docs#CategoryTheory.CategoryStruct, and then show it's associative when we have a category.) Another issue is that mathlib apparently doesn't have nonunital algebras yet, which path algebras can be.

[Bernhard Reinke]

Junyan Xu said:

Yes. Quivers doesn't have identity morphisms so eqToHom can't be defined. Here's a construction of the SemigroupWithZero; you probably want to directly construct an Algebra from the Semigroup instead of needlessly adjoining a zero element though.

import Mathlib.Algebra.GroupWithZero.Defs
import Mathlib.Algebra.Group.WithOne.Defs
import Mathlib.CategoryTheory.PathCategory.Basic

open CategoryTheory
universe u
instance {V} [Quiver.{u+1} V] [DecidableEq V] :
    SemigroupWithZero (WithZero (Σ v : Paths V × Paths V, v.1 ⟶ v.2)) where
  mul := fun p q ↦ p.rec 0 fun p ↦ q.rec 0 fun q ↦ if eq : p.1.2 = q.1.1 then
    some ⟨(p.1.1, q.1.2), p.2 ≫ eqToHom eq ≫ q.2⟩ else 0
  mul_assoc := sorry
  zero := 0
  zero_mul _ := rfl
  mul_zero := by rintro ⟨⟩ <;> rfl

Thanks for the stub! Regarding eqToHom, I meant something using Quiver.Path, not the path category. You can of course define something of the forma = b -> Path a b, but this is not in Quiver.Cast. Using the path category is probably cleaner

[Bernhard Reinke]

I think the way to go is defining a category algebra of a k-linear category. But I am not sure whether k-linear categories are already in mathlib

[Bernhard Reinke]

Oh, they are : docs#CategoryTheory.Linear

[Bernhard Reinke]

But I haven't found the free linear category of a category yet

[Mitchell Lee]

The path algebra of a quiver can be defined without ever using the word "path". It can be generated as an algebra by generators $x_v$ and $y_e$, where $v$ ranges over all vertices and $e$ ranges over all edges. It is not too difficult to write down the necessary relations. You may find this approach easier.

[Mitchell Lee]

See Problem 2.8.6 here: https://math.mit.edu/~etingof/reprbook.pdf

[Mitchell Lee]

With this approach, it is probably easier to prove the key theorem that the category of representations of a quiver is equivalent to the category of representations of its path algebra.

[Kim Morrison]

Bernhard Reinke said:

But I haven't found the free linear category of a category yet

https://leansearch.net/?q=The%20free%20linear%20category%20on%20a%20category%3F

[Kim Morrison]

docs#CategoryTheory.Free

[Bernhard Reinke]

I have created a WIP PR at #22809. In particular the path algebra part is just the definition so far. For the category algebra I managed to prove associativity using distributivity, the most abstract part I put in the new fileMathlib.Algebra.Ring.Assoc. I don't know whether it deserves its own file, but maybe one can also start putting the theory of the associator (as in (x*y)*z - x*(y*z)for non-associative rings) there.

[Bernhard Reinke]

Does it make sense to split this into 3 PRs (one for Mathlib.Algebra.Ring.Assoc, one for Mathlib.CategoryTheory.Linear.CategoryAlgebraand one for the path algebra itself)?

[Bernhard Reinke]

Ok, the definition of the associator is now in #22823