Zulip Chat Archive

Stream: Is there code for X?

Topic: Grp is not CCC


Kenny Lau (Jun 16 2020 at 04:43):

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

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)

Bhavik Mehta (Jun 16 2020 at 04:51):

I think this could be a fun kata

Kenny Lau (Jun 16 2020 at 04:51):

well the mathlib in CW isn't up to date

Kenny Lau (Jun 16 2020 at 04:52):

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

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.

Reid Barton (Jun 17 2020 at 20:53):

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

Scott Morrison (Jun 18 2020 at 00:42):

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

Reid Barton (Jun 18 2020 at 00:43):

just 10 years later

Kenny Lau (Jun 18 2020 at 05:24):

We need an "is_trivial" predicate for categories

Kenny Lau (Jun 18 2020 at 05:25):

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

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

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"

Kevin Buzzard (Jun 18 2020 at 06:38):

Why is that statement ever of any use?

Kevin Buzzard (Jun 18 2020 at 06:38):

It's just a zany example sheet question

Scott Morrison (Jun 18 2020 at 09:47):

Yeah, is_trivial C is surely just C ≌ punit.

Kenny Lau (Jun 18 2020 at 09:48):

what would the characteristic properties be?

Kenny Lau (Jun 18 2020 at 09:48):

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

Mario Carneiro (Jun 18 2020 at 09:57):

that looks more like a subsingleton than a singleton

Mario Carneiro (Jun 18 2020 at 09:57):

not sure which is more appropriate in this situation though

Kenny Lau (Jun 18 2020 at 09:59):

the counter-example is discrete bool

Mario Carneiro (Jun 18 2020 at 10:00):

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

Kenny Lau (Jun 18 2020 at 10:01):

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

Mario Carneiro (Jun 18 2020 at 10:02):

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

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

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

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.

Kenny Lau (Jun 18 2020 at 10:03):

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

Mario Carneiro (Jun 18 2020 at 10:03):

I think you are right

Kenny Lau (Jun 18 2020 at 10:04):

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

Kenny Lau (Jun 18 2020 at 10:04):

is a group trivial as a one-object category?

Mario Carneiro (Jun 18 2020 at 10:05):

is the empty category trivial?

Mario Carneiro (Jun 18 2020 at 10:06):

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

Kenny Lau (Jun 18 2020 at 10:15):

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

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

Kenny Lau (Jun 18 2020 at 10:30):

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

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

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.

Bhavik Mehta (Nov 06 2020 at 19:03):

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

Bhavik Mehta (Nov 06 2020 at 19:03):

oops I linked to the wrong MO post :)


Last updated: Dec 20 2023 at 11:08 UTC