Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: theory: category theory

Topic: strict factorization systems as strict algebras


view this post on Zulip Matteo Capucci (he/him) (Jul 04 2024 at 15:18):

Koronstenski & Tholen and Grandis showed that various flavours of factorization systems (FS) can be presented as various flavours of algebras of the 2-monad ()(-)^\downarrow on Cat\bf Cat, endowed with the obvious structure.
I wrote up Grandis' argument on the nLab. He says a strict algebra of ()(-)^\downarrow is a strict FS. When unpacking this statement, however, is clear that an algebra (X,t)(X,t) for the pointed endofunctor ((),η)((-)^\downarrow, \eta) is enough to recover a strict FS: tt provides factorizations and unitality (t.η=1t.\eta = 1) guarantees these are indeed factorizations. Uniqueness is trivial from the way we built the factorization.
K&T treat a similar thing in §2, calling it a weak FS. More precisely, they call WFS a pseudoalgebra of ((),η)((-)^\downarrow, \eta) and then claim one can always strictify such, so they work with strict algebras from there on.
Ultimately, this is because associativity can be proven from unitality as I sketched in the nLab write up.

But I must be getting something wrong: both K&T and Grandis prove an OFS is a strictly unital (i.e. normal) pseudoalgebra for the 2-monad ()(-)^\downarrow, but then what role does the associator play? We already know that carrier + strict unitality implies a strict factorization, why isn't every normal pseudoalgebra strict then?

view this post on Zulip Matteo Capucci (he/him) (Jul 04 2024 at 15:19):

This is going to be one of those cases where I'm drowning in an inch of water but here we are