Zulip Chat Archive

Stream: maths

Topic: categorical product


view this post on Zulip Kenny Lau (Jul 03 2019 at 07:36):

Is there a category CC such that:
1. For every discrete category DD and functor F:DCF:D\to C, FF has a limit (i.e. every sub-multi-set of Obj(C) has limit).
2. CC has no product, i.e. there is no functor F:C×CCF : C \times C \to C such that the induced natural transformation Hom(A,B) x Hom(A,C) -> Hom(A,F(B,C)) between two functors Cop×C×CSetC^{op} \times C \times C \to Set is a natural isomorphism

view this post on Zulip Mario Carneiro (Jul 03 2019 at 07:59):

Using D=2D={\bf 2}, we know that CC has a product object A×BA\times B for all A,BObj(C)A,B\in Obj(C). Pick one for every pair A,B to obtain a functor ×:C×CC\times:C\times C\to C. (The object part of this is obvious, and if f:AA,g:BBf: A\to A', g:B\to B' then f×g:=[fπA,B1,fπA,B2]A,Bf\times g := [f\circ \pi^1_{A,B}, f\circ \pi^2_{A,B}]_{A',B'}.) Then we can define ϕ(f:AB,g:AC):=[f,g]B,C:AB×C\phi(f:A\to B, g:A\to C) := [f, g]_{B,C}:A\to B\times C and ϕ1(h:AB×C):=(πB,C1h,πB,C2h)\phi^{-1}(h:A\to B\times C) :=(\pi^1_{B,C}\circ h, \pi^2_{B,C}\circ h) and this is an isomorphism.

In short, the only tricky part is using the axiom of choice to pick a product for every pair of objects. After that it's just equating two ways to say "a category with products".

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:28):

what if Obj(C) is a class...?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:32):

Then you have to be more careful about what you mean

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:32):

is there a class that has no choice function?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:32):

What's a category? What's a functor? What's an existential quantification over classes?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:33):

large category theory in ZFC is tricky

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:33):

I see

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:34):

For some choice of definitions, I think it's possible that you can have the existential statement 1 without any concrete functor class term refuting 2

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:34):

You can't prove 2 though because it's a higher order statement

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:35):

ZFC does not prove the existence or nonexistence of a class with no choice function

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:36):

Assuming that all classes have a choice function is usually called "global choice" and is morally equivalent to Lean's choice

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:36):

does V\{{}} admit a choice function?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:36):

that's also global choice

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:36):

I don't like this

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:37):

it's all because of Russell

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:37):

You can't prove it in ZFC because it is a higher order statement, it asserts the existence of a class term

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:38):

You can axiomatize global choice by saying "here is a class term, I assert it is a choice function on V"

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:38):

what if we only look at first order sentences?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:38):

That is a first order statement - the "class term" can be replaced by a primitive unary predicate

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:39):

It's conservative over ZFC

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:40):

is there a sentence in two variables φ(x,y)\varphi(x,y) such that x[x[!yφ][yφyx]]\forall x[x \ne \varnothing \implies [\exists! y \varphi] \land [\forall y \varphi \implies y \in x]]

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:40):

Not in ZFC

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:41):

why not?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:41):

choice is not definable

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:41):

is that a theorem?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:41):

yes

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:41):

how hard is it?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:41):

For instance, there is no definable well order of the reals

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:42):

Not actually sure who to credit for it

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:42):

so for example this implies V=L?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:44):

Here's a proof: https://math.stackexchange.com/a/1315720

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:44):

It doesn't imply V=L

view this post on Zulip Mario Carneiro (Jul 03 2019 at 08:46):

It certainly "enlarges" L but you still can't prove that all sets are constructible without parameters

view this post on Zulip Kenny Lau (Jul 03 2019 at 08:47):

ok thanks


Last updated: May 11 2021 at 15:12 UTC