Skip to main content

Definitions in the liquid tensor experiment

Community projects

A few weeks ago, we announced the completion of the liquid tensor experiment (LTE for short). What this means is that we stated and (completely) proved the following result in Lean:

variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)]

theorem liquid_tensor_experiment 
  (S : Profinite) (V : pBanach p) :
  ∀ i > 0, Ext i (ℳ_{p'} S) V ≅ 0 :=
-- the proof ...

The code block above, which is taken directly from the file challenge.lean in the main LTE repository, uses some custom notation to make the statement appear as close as possible to the main theorem mentioned in Scholze's original challenge. Fortunately, it's relatively straightforward to unravel the notation to see the underlying definitions themselves. But there is a bigger issue: How can we convince ourselves (and others) that the definitions we introduced in LTE are actually correct?

For instance, we could have defined Ext to be $0$ (spoiler: we didn't). Or, we could have made some subtle innocent mistake in setting up the definitions that somehow implies that Ext is always $0$, or that all condensed abelian groups are trivial, or one of several other pitfalls that renders the statement above meaningless.

To answer this question, we built a new examples folder in the repository which contains several files corresponding to the main players in the statement above. These examples can be considered as centralized "sanity checks" that the definitions we wrote using Lean actually behave as expected.

We tried to write the files in this folder in a way which should be (approximately) readable by mathematicians who have minimal experience with Lean. The goal is to make it easy for non-experts to look through the examples folder, then look through the concise final statement in challenge.lean, and be reasonably confident that the challenge was accomplished.

This blog post gives a detailed overview of this folder and its contents, and how it relates to the definitions used in the main statement of the liquid tensor experiment. It is meant to be read alongside the actual files from the examples folder.

Read more…

Classification of one-dimensional isocrystals

New in mathlib

Last year, there was a big mathlib refactor to replace linear maps throughout the library with semilinear maps, a more abstract concept which, importantly, unifies linear and conjugate-linear maps.

But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should make sure we chose this full generality of semilinear maps, maps $f:M \to N$ such that $f(ax)=\sigma(a)f(x)$ for some ring homomorphism $\sigma$ between the scalar rings of the modules $M$ and $N$. So we and our coauthor Frédéric Dupuis implemented this full generality, and then asked them for an example to illustrate their need for this more abstract definition. This blog post tells the story of our little adventure in number theory.

It turns out that the standard use of semilinear maps in number theory is for Frobenius-semilinearity, semilinearity with respect to the ring homomorphism of the fraction field of the $p$-typical Witt vectors over a perfect characteristic-$p$ integral domain which is induced by the Frobenius automorphism of that domain. Let's backtrack to catch everyone up...

Read more…