One-object category

Stream: maths

[Yury G. Kudryashov]

Hi, do we have a way to turn any monoid into End of a one-object category? I want to prove some facts for categories, then transfer them to monoids. It shouldn't be hard to define such thing (e.g., using a type tag on unit) but I'd prefer not to reinvent the wheel.
BTW, if this type tag does not exist yet, what would be a good name for it?

[Johan Commelin]

Is there standard notation for this in maths?

[Johan Commelin]

I know BG for groups...

[Johan Commelin]

Maybe monoid.categorify?

[Yury G. Kudryashov]

Algebra is not my field of study, and I failed to find standard notation.

[Yury G. Kudryashov]

Let it be monoid.categorify

[Scott Morrison]

I'm not sure what exactly you're proposing here, so I can't help with the name.

[Yury G. Kudryashov]

@Scott Morrison I want to have def my_type_tag : Type u → Type := λ _, unit with instance : category_theory.has_hom (my_type_tag α) := { hom : λ _ _, α } and instance : category_theory.category_struct {α} [monoid α] (my_type_tag α) := { id := λ _, 1, comp := λ _ _ _ x y, x * y } (probably with some changes to make this code work).

[Scott Morrison]

oh! I see.

[Scott Morrison]

I would call it turtle, but that is very idiosyncratic. (Say a "k-boring n-category" is an n-category such that there is a unique j-morphism for j <= k. As examples, monoids are 1-boring 1-categories, monoidal categories are 1-boring 2-categories, and braided monoidal categories are 2-boring 3-categories, and symmetric monoidal categories are k-boring (k+1)-categories for any k >= 3. Whenever I need to name these otherwise nameless unique morphisms, I call them "turtle", because "it's turtles all the way down".)

[Yury G. Kudryashov]

Sorry, I know nothing about n-categories. After reading an intro part of the Wikipedia page, it seems that 1-categories are just categories. Then 1-boring 1-categories are categories such that there is a unique morphism (same as 1-morphism?). But I need one object, not one morphism. Do I miss something?

[Scott Morrison]

Ah: "0-morphisms" just means "objects", so a 1-boring 1-category is exactly a monoid.

[Yury G. Kudryashov]

Then you probably mean "for j < k", not "for j ≤ k".
The main issue with the name "turtle" is that it seems to be neither a standard term in math, nor a descriptive word. May be, "categorify" is better.

[Scott Morrison]

Yes, you're right, <, not <=.

[Scott Morrison]

The problem is that "categorify" means something specific, and it isn't this.

[Scott Morrison]

X, an n-category, is a categorification of Y, an (n-1)-category, if when you throw out the n-morphisms in X, and replace the n-1 morphisms with isomorphism classes, you get Y.

[Scott Morrison]

So for example the monoidal category Vec is a categorification of the monoid nat under multiplication.

[Yury G. Kudryashov]

OK, then one_obj_category.

[Yury G. Kudryashov]

I've just realized that the "public" function will turn α into α interpreted as End unit.star in this category. Probably, it should be called as_End or to_End.

[David Michael Roberts]

The delooping of a monoid is a one-object category (because the 'loops' in the category are exactly the elements of the monoid)

[Yury G. Kudryashov]

What is delooping? Is it already in mathlib?

[Jesse Michael Han]

see section 6 of this nLab article (it means what you think it means)

[Jesse Michael Han]

or as some people are fond of saying, "a category is just a monoidoid!"

[Yury G. Kudryashov]

@Jesse Michael Han I'm lost after a few lines (have to lookup the meaning of every other word). I think, I'll define the single object category in a straightforward manner; if someone will define delooping in a general context later, it would be easy to prove equivalence in this particular case, or even replace my definition.

[Jesse Michael Han]

yeah that should be fine; for the case of monoid -> one object category, it's hard to go wrong

[Johan Commelin]

@Scott Morrison What do you think about composition getting all messed up now that we try to mix category theory and the rest of the library?

[Johan Commelin]

I know that there is only one right way to do compositions, and it is the one that is used in the category theory library.

[Johan Commelin]

However, if I had to choose between converting the world to "the one right composition" or "formalisation of maths", then I would choose the latter.

[Johan Commelin]

At the moment, I think this is actively confusing for people.

[Johan Commelin]

Is the composition order in category_theory open for debate?

[Scott Morrison]

Sure, of course.

[Scott Morrison]

My suggestion would be to not change anything, just chose a new unicode symbol for morphism-composition that looks not entirely unlike \circ, and define two notations.

[Scott Morrison]

One could later rip out use of the \gg notation if desired, but I don't think there's any need to change the underlying form of category.comp. Or is there?

[Scott Morrison]

As far as I'm aware, this is purely a notational mismatch.

[Johan Commelin]

I think technically it is a notational mismatch. But there is also a psychological component. Several people (mathematicians working in algebra/geometry) whom I've showed Lean/mathlib were quite confused by the convention.

[Johan Commelin]

But have some circ-like symbol might be a good start.

[Scott Morrison]

There's the degree symbol, which is typeset a bit higher than the usual \circ, e.g. as f ° g.

[Scott Morrison]

Or there's ⊚

[Scott Morrison]

which you can already type as \oo