Zulip Chat Archive

Stream: Is there code for X?

Topic: Grp is not CCC


view this post on Zulip Kenny Lau (Jun 16 2020 at 04:43):

Do we know that Grp (the category of groups) is not a Cartesian Closed Category (CCC)?

view this post on Zulip Kenny Lau (Jun 16 2020 at 04:50):

this boils down to producing three groups A, B, C with (AB)×C(A×C)(B×C)(A \ast B) \times C \ncong (A \times C) \ast (B \times C)

view this post on Zulip Bhavik Mehta (Jun 16 2020 at 04:51):

I think this could be a fun kata

view this post on Zulip Kenny Lau (Jun 16 2020 at 04:51):

well the mathlib in CW isn't up to date

view this post on Zulip Kenny Lau (Jun 16 2020 at 04:52):

btw A = B = C1, C = C2, by cardinality arguments

view this post on Zulip Valery Isaev (Jun 17 2020 at 20:36):

I think it's easier to show XX1=X01X \simeq X^1 = X^0 \simeq 1, which shows that any CCC with a zero object is trivial.

view this post on Zulip Reid Barton (Jun 17 2020 at 20:53):

https://mathoverflow.net/questions/10290/can-a-topos-ever-be-an-abelian-category

view this post on Zulip Scott Morrison (Jun 18 2020 at 00:42):

Once it's in mathlib, someone should post a comment to Reid's MO post. :-)

view this post on Zulip Reid Barton (Jun 18 2020 at 00:43):

just 10 years later

view this post on Zulip Kenny Lau (Jun 18 2020 at 05:24):

We need an "is_trivial" predicate for categories

view this post on Zulip Kenny Lau (Jun 18 2020 at 05:25):

is it the same as "category equivalence to 1"?

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 06:26):

We need an "is_trivial" predicate for categories

Why?

I remember once noting that in stark contrast to eg groups or graphs, there are no lists of finite categories of small size (that I know of, at least). Maybe it's because classifying them up to equivalence is the correct thing, not isomorphism? Nobody talks about the classification of categories of size at most 6, whatever size means

view this post on Zulip Kenny Lau (Jun 18 2020 at 06:29):

Kevin Buzzard said:

We need an "is_trivial" predicate for categories

Why?

to formalize the statement "any CCC with a zero object is trivial"

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 06:38):

Why is that statement ever of any use?

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 06:38):

It's just a zany example sheet question

view this post on Zulip Scott Morrison (Jun 18 2020 at 09:47):

Yeah, is_trivial C is surely just C ≌ punit.

view this post on Zulip Kenny Lau (Jun 18 2020 at 09:48):

what would the characteristic properties be?

view this post on Zulip Kenny Lau (Jun 18 2020 at 09:48):

maybe something like \forall x y : C, unique (X \hom Y)?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 09:57):

that looks more like a subsingleton than a singleton

view this post on Zulip Mario Carneiro (Jun 18 2020 at 09:57):

not sure which is more appropriate in this situation though

view this post on Zulip Kenny Lau (Jun 18 2020 at 09:59):

the counter-example is discrete bool

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:00):

counterexample to what? I'm not sure which definition you are working with

view this post on Zulip Kenny Lau (Jun 18 2020 at 10:01):

discrete bool is a category that satisfies the subsingleton condition but is not trivial

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:02):

discrete bool looks equivalent to punit to me, if I understand categorical equivalence correctly

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:02):

in fact that's the canonical example when showing that equivalence is not the same as isomorphism

view this post on Zulip Scott Morrison (Jun 18 2020 at 10:03):

No, it isn't, because if you send * to ff, tt will be sent to * and then back to ff, which is not isomorphic to tt

view this post on Zulip Scott Morrison (Jun 18 2020 at 10:03):

Mario, I think you're thinking indiscrete bool (which we don't have) but which is equivalent to punit.

view this post on Zulip Kenny Lau (Jun 18 2020 at 10:03):

#Hom(ff,tt) = 0 while #Hom(*,*) = 1

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:03):

I think you are right

view this post on Zulip Kenny Lau (Jun 18 2020 at 10:04):

theorem: C is trivial iff C is isomorphic to indiscrete C

view this post on Zulip Kenny Lau (Jun 18 2020 at 10:04):

is a group trivial as a one-object category?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:05):

is the empty category trivial?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:06):

it is not equivalent to punit but it is isomorphic to indiscrete empty

view this post on Zulip Kenny Lau (Jun 18 2020 at 10:15):

revised theorem: C is trivial iff C is nonempty and isomorphic to indiscrete C

view this post on Zulip David Wärn (Jun 18 2020 at 10:21):

It seems you fell into the old trap of characterising "pretrivial" categories! That gives (-1)-categories, whereas you want (-2)-categories

view this post on Zulip Kenny Lau (Jun 18 2020 at 10:30):

@David Wärn what do those terms mean in English?

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 10:35):

Equivalence means bijective on hom sets and bijective on iso classes of objects, so equivalent to trivial means one iso class of objects and a unique iso between each pair

view this post on Zulip David Wärn (Jun 18 2020 at 10:54):

Kenny Lau said:

David Wärn what do those terms mean in English?

I was just observing that this is the "too simple to be simple" thing. When you define, say, connected graphs, the obvious thing to say is "for any two vertices there is a path", but you don't want the empty graph to be connected. It's the relation between subsingleton and singleton. I'm using "pretrivial" analogously to mathlib's "preconnected" and "preirreducible", so "pretrivial" is to "trivial" what "subsingleton" is to "singleton".

Roughly speaking, and working up to equivalence, if you accept that a (-2)-category is just punit, then a (-1)-category is a category where all the hom-sets are (-2)-categories, i.e. for any two objects there is a unique hom, i.e. the category is punit or empty. Then a 0-category is where the hom-sets are (-1)-categories, i.e. punit or empty, so a 0-category is a discrete category. Then a 1-category is just an ordinary category.

view this post on Zulip Bhavik Mehta (Nov 06 2020 at 19:03):

https://github.com/leanprover-community/mathlib/pull/4924

view this post on Zulip Bhavik Mehta (Nov 06 2020 at 19:03):

oops I linked to the wrong MO post :)


Last updated: May 07 2021 at 19:12 UTC