Light condensed sets

Stream: condensed mathematics

[Dagur Asgeirsson]

Dustin and Peter are giving a lecture series called "analytic stacks", which describes new foundations for analytic geometry built on light condensed sets (see here).

These light condensed sets are sheaves on a category which is essentially small, getting rid of all the set theoretic problems in condensed sets and simplifying the basics of the solid (and probably also liquid) theory.

I just opened a PR with the definition of light condensed objects: #8717. It depends on quite a few other PRs, but comments and suggestions are very welcome!

The problem with defining sheaves on large sites is that you need a universe bump to be able to sheafify. This is a priori still true for large essentially small categories in Lean, so we still need to do some work with transferring sheaves over equivalences of the defining sites to actually get a small sheaf when we sheafify.

[Yaël Dillies]

So they are light _and_ condensed? What are they made of!

[Junyan Xu]

https://en.m.wikipedia.org/wiki/Condensed_aerosol_fire_suppression