## 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 $(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 $X \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

#### 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: May 07 2021 at 19:12 UTC