Zulip Chat Archive

Stream: maths

Topic: does CCC preserve category equivalence


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

if C and D are equivalent categories and C is CCC, does it follow that D is also CCC?

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

(CCC = Cartesian Closed Category)

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

Yup, this is in mathlib already :)

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

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/closed/cartesian.lean#L324

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

then your goal that Type u is CCC follows from a more general theorem that if C is CCC then C => Type u (the category of functors) is CCC

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

Sure, but I don't have the latter yet

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

And I've done the former

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

(Largely to make sure my definition of CCC made sense)

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

well but I think in mathlib we prove the most general things first

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

Also, C => Type u being CCC doesn't need C to be CCC

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

oops

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

Yeah and that's why I haven't made a PR yet :)

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

Oh actually I already have done that C^op => Type u is CCC

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

then you can deduce that C => Type u is CCC :P

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

it's a pretty horrible proof though - if we're going for the most general thing then really we should show C^op => Type u is comonadic over Type u, and the category of coalgebras over a CCC is CCC

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

do we know that empty and 1 are CCCs?

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

We don't have any CCCs in mathlib right now

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

then maybe I can PR the empty case

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

(is empty a category?)

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

Yeah, it's called pempty

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

ok I'll work on the pempty case

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

If you desperately want more examples I can post my presheaf category version for now

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

failed to synthesize type class instance for
 category pempty

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

which file should I import?

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

category_theory.pempty, I think

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

oh no pempty is not CCC

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

guess why

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

oh terminal doesn't exist

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

bingo

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

import category_theory.closed.cartesian
import category_theory.punit

universe u

namespace category_theory

instance : limits.has_finite_products.{u u} punit :=
{ has_limits_of_shape := λ J _ _,
  { has_limit := λ F,
    { cone := { X := punit.star,
                π := { app := λ X, punit.star } },
      is_limit := { lift := λ s, punit.star } } } }

instance : cartesian_closed.{u u} punit :=
{ closed := λ X,
  { is_adj :=
    { right := { obj := id, map := λ _ _, id },
      adj :=
      { hom_equiv := λ _ _, equiv.refl punit,
        unit := { app := id },
        counit := { app := id } } } } }

end category_theory

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

yay

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

But doesn't this follow from C => Type u being CCC? ;)

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

:octopus:


Last updated: May 06 2021 at 17:38 UTC