Grp is not CCC

Stream: Is there code for X?

[Kenny Lau]

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

[Kenny Lau]

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]

I think this could be a fun kata

[Kenny Lau]

well the mathlib in CW isn't up to date

[Kenny Lau]

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

[Valery Isaev]

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]

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

[Scott Morrison]

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

[Reid Barton]

just 10 years later

[Kenny Lau]

We need an "is_trivial" predicate for categories

[Kenny Lau]

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

[Kevin Buzzard]

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]

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]

Why is that statement ever of any use?

[Kevin Buzzard]

It's just a zany example sheet question

[Scott Morrison]

Yeah, is_trivial C is surely just C ≌ punit.

[Kenny Lau]

what would the characteristic properties be?

[Kenny Lau]

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

[Mario Carneiro]

that looks more like a subsingleton than a singleton

[Mario Carneiro]

not sure which is more appropriate in this situation though

[Kenny Lau]

the counter-example is discrete bool

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

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

[Kenny Lau]

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

[Mario Carneiro]

I think you are right

[Kenny Lau]

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

[Kenny Lau]

is a group trivial as a one-object category?

[Mario Carneiro]

is the empty category trivial?

[Mario Carneiro]

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

[Kenny Lau]

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

[David Wärn]

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

[Kenny Lau]

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

[Kevin Buzzard]

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]

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]

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

[Bhavik Mehta]

oops I linked to the wrong MO post :)