ingredients

Stream: condensed mathematics

[Johan Commelin]

I'm preparing a talk on LTE, and I thought it would be nice to give a list of "Ingredients".
Here's what I came up with, of the top of my head:

  the real numbers, normed groups, $p$-Banach spaces,
  locally constant functions, completions (of metric spaces),
  absolute convergence and infinite sums,
  pseudo-normed groups, abelian categories, homological complexes, homotopies, the snake lemma,
  profinite sets, \v Cech covers, the normalized Moore complex,
  polyhedral lattices, Gordan's lemma,
  derived functors, long exact sequences, more homological algebra,
  condensed sets, extremally disconnected sets, sheaves, more topos theory,
  condensed abelian groups, some form of Breen--Deligne resolutions

Am I missing anything?

[Johan Commelin]

I left out things that are so specific to this proof that they don't make much sense outside of it.

[Riccardo Brasca]

LGTM, at least concerning the parts I've contributed to.

[Kevin Buzzard]

Binary expansion of a positive real number!

[Johan Commelin]

Thanks, I'll add it.

[Yaël Dillies]

This definitely features in the category of stupid prerequisites we should have had for a long time :grinning: Thanks Kevin!

[Kevin Buzzard]

You can see progress in some files called things like nnreal_nat_binary.lean in for_mathlib directory in LTE

[Filippo A. E. Nuccio]

I think you could mention cones of functors (at least as limits). Or does it count in your "sheaves" or "topos theory"?

[Adam Topaz]

We used the fact that filtered colimits commute with finite limits about 37 times. Maybe there should be a lots of category theory category ;)

[Scott Morrison]

You're welcome. :-)