## Stream: Is there code for X?

### Topic: kTop is CCC

#### Kenny Lau (Jun 16 2020 at 04:01):

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

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

#### 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?

#### 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

#### Johan Commelin (Jun 16 2020 at 06:39):

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

#### Kenny Lau (Jun 16 2020 at 06:41):

what is the condensed repo?

#### Johan Commelin (Jun 16 2020 at 07:04):

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

#### Johan Commelin (Jun 16 2020 at 07:04):

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

#### 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.

#### 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 $\mathbb{R}^n$).

Last updated: May 16 2021 at 05:21 UTC