Normed homological algebra

Clausen and Scholze are developing new foundations for analytic geometry that accommodate both archimedean objects (e.g., complex manifolds) and nonarchimedean ones (e.g., Huber's adic spaces) in a common framework. The building blocks of this theory are called analytic rings. Constructing archimedean analytic rings relies on the "main theorem of liquid vector spaces", whose proof was formalized in the Lean theorem prover in 2022 (the "Liquid Tensor Experiment"). One of many ingredients in this proof is a variant of homological algebra in which equations are systematically replaced by approximations, with specific bounds on the norms of the errors.

I will give a brief introduction to analytic rings, then describe how theorems of ordinary homological algebra can be transported to the normed setting using methods from mathematical logic. This is based on joint work with Johan Commelin.