Stream: maths

Topic: One-object category

Yury G. Kudryashov (Jul 05 2019 at 18:25):

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 (Jul 05 2019 at 18:30):

Is there standard notation for this in maths?

Johan Commelin (Jul 05 2019 at 18:30):

I know BG for groups...

Johan Commelin (Jul 05 2019 at 18:33):

Maybe monoid.categorify?

Yury G. Kudryashov (Jul 05 2019 at 18:35):

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

Yury G. Kudryashov (Jul 05 2019 at 18:36):

Let it be monoid.categorify

Scott Morrison (Jul 05 2019 at 20:12):

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

Yury G. Kudryashov (Jul 05 2019 at 20:28):

@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).

oh! I see.

Scott Morrison (Jul 05 2019 at 20:33):

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 (Jul 05 2019 at 20:44):

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 (Jul 05 2019 at 20:58):

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

Yury G. Kudryashov (Jul 05 2019 at 21:02):

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 (Jul 05 2019 at 21:09):

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

Scott Morrison (Jul 05 2019 at 21:09):

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

Scott Morrison (Jul 05 2019 at 21:14):

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 (Jul 05 2019 at 21:15):

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

Yury G. Kudryashov (Jul 05 2019 at 21:17):

OK, then one_obj_category.

Yury G. Kudryashov (Jul 05 2019 at 21:23):

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 (Jul 14 2019 at 11:27):

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 (Jul 14 2019 at 12:21):

What is delooping? Is it already in mathlib?

Jesse Michael Han (Jul 14 2019 at 12:31):

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

Jesse Michael Han (Jul 14 2019 at 12:32):

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

Yury G. Kudryashov (Jul 14 2019 at 13:32):

@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 (Jul 14 2019 at 14:03):

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

Johan Commelin (Jul 22 2019 at 01:26):

@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 (Jul 22 2019 at 01:27):

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 (Jul 22 2019 at 01:27):

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 (Jul 22 2019 at 01:28):

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

Johan Commelin (Jul 22 2019 at 01:28):

Is the composition order in category_theory open for debate?

Sure, of course.

Scott Morrison (Jul 22 2019 at 01:38):

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 (Jul 22 2019 at 01:38):

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 (Jul 22 2019 at 01:39):

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

Johan Commelin (Jul 22 2019 at 01:42):

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 (Jul 22 2019 at 01:42):

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

Scott Morrison (Jul 22 2019 at 02:11):

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

Scott Morrison (Jul 22 2019 at 02:12):

Or there's ⊚

Scott Morrison (Jul 22 2019 at 02:13):

which you can already type as \oo

Last updated: May 14 2021 at 20:13 UTC