kTop is CCC

Stream: Is there code for X?

[Kenny Lau]

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

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

[Kenny Lau]

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]

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]

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

[Kenny Lau]

what is the condensed repo?

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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$).

[Boris Kjær]

I was wondering if there is any news on this?

[Adam Topaz]

Is it even worth formalizing kTop, or should we do the right thing and go with condensed sets from the beginning?

[Reid Barton]

I never saw anyone trying to do homotopy theory with condensed sets. Though I think they should have a Kan-Quillen-style model structure. Johan and I were talking about this a bit recently actually.

[Johan Commelin]

There is https://mathoverflow.net/questions/416963/homotopy-theory-with-condensed-sets which links to https://arxiv.org/abs/2105.07888.

[Dagur Ásgeirsson]

The functor Top_to_Condensed is fully faithful when restricted to this category kTop (proposition 1.7 in Condensed.pdf , where these spaces are called compactly generated). Did LTE formalise anything like this? Boris and I are trying to formalise a result about discreteness of condensed sets which, given that proposition, can be reduced to something like: a topological space is discrete iff it is compactly generated and every continuous map to it from a profinite set has finite discrete image.

[Johan Commelin]

@Adam Topaz is the expert on that part of LTE. I think faithful might be done. But I'm not sure.

[Johan Commelin]

Hmmm, a simple grep doesn't find anything.

[Adam Topaz]

yeah we didn't do that in LTE. We do have the functor from Top to Condensed Type* here:
https://github.com/leanprover-community/lean-liquid/blob/92f188bd17f34dbfefc92a83069577f708851aec/src/condensed/top_comparison.lean#L126
It should be fairly straightforward to see that the restriction to compactly generated topological spaces is fully faithful

[Adam Topaz]

I want to start moving some condensed stuff to mathlib, but I've been avoiding doing so because of the ongoing port to Lean4.

[Scott Morrison]

Isn't the ongoing port to Lean4 a reason to do the move? Last chance to save this code, etc.

[Adam Topaz]

Maybe. The way i see it, rotting code in LTE is essentially equivalent to rotting code in the non-ported parts of mathlib3. So as long as the prerequisite parts of mathlib3 get ported, it wouldn't matter either way.

[Adam Topaz]

Plus, I would prefer to devote my (currently nonexistent) lean-code-writing time to porting instead of new mathlib3 prs.