Some enriched/2-category theory

Stream: mathlib4

[Brendan Seamas Murphy]

I would like to develop the following, in no particular order:

• An appropriate sort of equivalence between strict 2-categories and Cat-enriched categories
• The cartesian closed structure on Cat
• The self enrichment of a closed monoidal category
• The cartesian closed structure of preorders, posers
• The enrichment of various categories of ordered things in Preord/Pos
• The induced strict 2-category structures from the above

Is anyone else working on related things, and separately does anyone have feedback/suggestions on this vague plan of action?

[Brendan Seamas Murphy]

I also think it would be nice to have a notion of "concrete monoidal category", where the data of a concrete monoidal structure on a monoidal category $(\mathcal{C}, \otimes, k)$ is a concrete category structure on $\mathcal{C}$, i.e. a faithful functor $U : \mathcal{C} \to \mathsf{Set}$, and a universal element $\xi \in U(k)$ exhibiting that the unit object corepresents the forgetful functor. As far as I know this isn't a standard defintion. However I think it would be nice to be able to talk about how eg an Ab-enriched category is the same as an ordinary category + abelian group structures on Hom sets + a proof that composition is bilinear, or how a Poset-enriched category is an ordinary category + a partial order on Hom sets + a proof that composition is monotone. I don't know how people generally feel about adding nonstandard mathematical defintions to the library though, is it completely prohibited?

[Johan Commelin]

@Brendan Seamas Murphy don't worry, we do that all the time.

[Brendan Seamas Murphy]

cool! I did notice the documentation for monoidal closed categories pointing out that eg k-algebras could reasonably be called "concrete monoidal" but their forgetful functor is represented by k[X], not the unit k. So I'll hold off on that particular bit until I think about this harder and confirm with people on zulip it makes sense

[Johan Commelin]

Maybe it's enough if the forgetful functor is representable?

[Johan Commelin]

Or maybe not even that?

[Johan Commelin]

But I guess you'd want something :grinning:

[Brendan Seamas Murphy]

Bare minimum is that it's either lax or oplax monoidal

[Brendan Seamas Murphy]

The definition I initially suggested gives lax monoidal

[Brendan Seamas Murphy]

I think representability by a monoid gives lax monoidal generally? and maybe vice versa, by yoneda? Lax functors are the monoids in the functor category.

[Brendan Seamas Murphy]

I can't think of an example where it's oplax, but I'm uncertain

[Brendan Seamas Murphy]

I think lax makes more sense, it means there's a set-function X × Y -> X (×) Y and this says something like X (×) Y is generated by honest pairs (in a very loose way). Maybe it becomes clearer if things are recast in terms of the closed structure