Categorical foundations of formalized condensed mathematics

Stream: maths

[Dagur Asgeirsson]

@Riccardo Brasca, @Nikolas Kuhn, @Filippo A. E. Nuccio, @Adam Topaz, and myself, have written the paper Categorical foundations of formalized condensed mathematics about the process of establishing the category-theoretic framework necessary to do condensed mathematics in mathlib.

We prove some general results about sheaves on extensive, (pre)regular and (pre)coherent categories, recovering key results in the foundations of condensed mathematics. In many cases, these results were known, but not proved explicitly in the "correct generality". We provide these proofs in the informal text, along with links to the lean code which is already in mathlib.

The preprint can be found at https://hal.science/hal-04633614v1. Comments very welcome!

[David Loeffler]

Trivial observation: Dagur's affiliation is given as "Copenaghen" [sic].

[Dagur Asgeirsson]

Thanks!

[Markus Himmel]

On p.4, it says Type 1 = Type 2, which presumably should read Type 1 : Type 2

[Adam Topaz]

Oh man… we really should have type checked our paper

[Dagur Asgeirsson]

Who needs universes higher than 1? :joy:

[Markus Himmel]

The naming of saturate doesn't follow the mathlib naming conventions (it should be Saturate). This seems to be a bug in mathlib rather than the paper. By the way, the inline links to mathlib are really cool!

[Dagur Asgeirsson]

#14449 changes the name of saturate to Saturate