Zulip Chat Archive

Stream: maths

Topic: One-object category


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 05 2019 at 18:30):

Is there standard notation for this in maths?

view this post on Zulip Johan Commelin (Jul 05 2019 at 18:30):

I know BG for groups...

view this post on Zulip Johan Commelin (Jul 05 2019 at 18:33):

Maybe monoid.categorify?

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 18:35):

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

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 18:36):

Let it be monoid.categorify

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Jul 05 2019 at 20:29):

oh! I see.

view this post on Zulip 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".)

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Jul 05 2019 at 20:58):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 05 2019 at 21:09):

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

view this post on Zulip Scott Morrison (Jul 05 2019 at 21:09):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 05 2019 at 21:15):

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

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 21:17):

OK, then one_obj_category.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Yury G. Kudryashov (Jul 14 2019 at 12:21):

What is delooping? Is it already in mathlib?

view this post on Zulip Jesse Michael Han (Jul 14 2019 at 12:31):

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

view this post on Zulip Jesse Michael Han (Jul 14 2019 at 12:32):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 22 2019 at 01:28):

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

view this post on Zulip Johan Commelin (Jul 22 2019 at 01:28):

Is the composition order in category_theory open for debate?

view this post on Zulip Scott Morrison (Jul 22 2019 at 01:37):

Sure, of course.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Jul 22 2019 at 01:39):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 22 2019 at 01:42):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 22 2019 at 02:12):

Or there's

view this post on Zulip Scott Morrison (Jul 22 2019 at 02:13):

which you can already type as \oo


Last updated: May 14 2021 at 20:13 UTC