Suggestions for Thursday / Friday lectures

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

Adam and I have got through pretty much all of the material that we sketched out in the plan for the week. What should I be doing at 9am on Thursday? Shall I just take a random sorry in the repo and we can solve it together?

[Adam Topaz]

One option that came up in discussions over dinner yesterday: interpreting topological spaces, groups, etc, as condensed sets, condensed groups, etc.

Any other suggestions?

[Kevin Buzzard]

How far are we from doing any solid stuff @Dagur Ásgeirsson ?

[Kevin Buzzard]

I could definitely work on the functor from top spaces to condensed sets. Do we have the notion of a qcqs object

[Adam Topaz]

No re qcqs, but we could aim for that def as well

[Adam Topaz]

In my lecture today I didn’t get quite as far as I had expected. If not much progress was made on today’s targets, I could also pick it up where I left off today.

[Dagur Asgeirsson]

Regarding the functor from topological spaces to condensed sets:

I would like both functors Top.{u+1} --> CondensedSet.{u} and Profinite.{u} --> CondensedSet.{u+1}. In LTE, both were defined only from universe level u, but it surely exists for Top.{u+1} (I have some old lean 3 code for this, but we could as well do it from scratch).

The reason I still want the one from Profinite.{u} is that I want to be able to say that $X(S) \cong Hom_{CondensedSet}(S,X)$ for a profinite $S$ and condensed set $X$.

For solid, we need
(1) the category of condensed abelian groups to have all limits required to define right Kan extensions,
(2) the functor from Profinite.{u} mentioned above (or at least a functor from Fintype.{u}), and
(3) to be able to define "free condensed abelian groups" (at least on a finite set, but we should really define the left adjoint to the forgetful functor from CondAb to CondSet)

[Adam Topaz]

Limits for condab is easy and done in my file from today (maybe just as an example?)

[Adam Topaz]

Free cond ab is a matter of finding the right def from mathlib, there’s something about making adjunction a for sheaf cats from adjunctions for the target cats

[Kevin Buzzard]

Some things which came up over snacks this afternoon: if C and D are equivalent, then Cond(C) and Cond(D) are equivalent :-) What properties if any do you need on a functor from C to D in order to get a functor from Cond(C) to Cond(D)? If C has a monoidal structure, does Cond(C)?

[Adam Topaz]

Maybe for the next two days we can just go through the suggestions in this stream one by one ;)

[Kevin Buzzard]

That would be fine by me

[Adam Topaz]

Aka a tour of mathlib4 category theory

[Boris Kjær]

Announcement: We will have a visitor tomorrow. @David Thrane Christiansen will come (Thursday) and say hello and maybe say a few words about his book on Lean 4 and perhaps even say what a monad transformer is. This would take place after Adam's lecture before we go for lunch.

[David Thrane Christiansen]

:wave:

[Filippo A. E. Nuccio]

@Adam Topaz What about sketching a proof that Ab has AB5?