Zulip Chat Archive

Stream: Is there code for X?

Topic: kTop is CCC


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

kTop = the category of kk-spaces (a topological XX is called a kk-space if a subspace UXU \subseteq X is open if and only if the preimage t1(U)t^{-1}(U) is open for any compact Hausdorff space CC and continuous t:CXt : C \to X)

CCC = Cartesian Closed Categories (a category with an internal notion of functions) #2894

reference: https://ncatlab.org/nlab/show/compactly+generated+topological+space#cartesian_closure

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

  1. do we have k-spaces in Lean?
  2. do we have kTop (the category) in Lean?
  3. do we know that kTop is CCC in Lean?

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

Definitely not for 3, there's currently no instances of CCC in mathlib yet - I'm preparing a PR to show Type u is CCC and another for presheaf categories but as far as I know there aren't any others floating about

view this post on Zulip Johan Commelin (Jun 16 2020 at 06:39):

@Kenny Lau wasn't there a start on compactly generated things in the condensed repo?

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

what is the condensed repo?

view this post on Zulip Johan Commelin (Jun 16 2020 at 07:04):

https://github.com/ImperialCollegeLondon/condensed-sets

view this post on Zulip Johan Commelin (Jun 16 2020 at 07:04):

It's a long time I did anything in that repo

view this post on Zulip Reid Barton (Jun 16 2020 at 11:35):

I have some super old code for this that predates category theory in mathlib, but I think it essentially does 1-3.

view this post on Zulip Reid Barton (Jun 16 2020 at 11:37):

It's worthwhile to be general in the "probe" spaces--not just the family of compact spaces, but an arbitrary family (for the most part, a smaller family like metric spaces or the spaces Rn\mathbb{R}^n).


Last updated: May 16 2021 at 05:21 UTC