semilinear-paper

Formalized functional analysis with semilinear maps

This site documents the code for the paper Formalized functional analysis with semilinear maps by Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth, published in the proceedings of ITP 2022. For the updated journal version, see here.

Where to find our code

All of the code that we describe in our paper is available on the semilinear-paper-update branch of the mathlib repository. This branch is frozen at the date of submission of the camera-ready version. We maintain a backup at another repository

Much of the code we decribe is already integrated into the master branch of the mathlib repository. The only pieces remaining to be integrated are the proofs of the spectral theorems. You can view the diff between the semilinear-paper-update branch and the master branch at the time of submission.

To download the code and explore it yourself:

Install Lean
leanproject get mathlib:semilinear-paper-update
Use VSCode’s Open folder feature, or code mathlib_semilinear-paper-update/, to open the root of the mathlib repository.
- You CANNOT interactively browse a single file by opening it in VSCode. You MUST open the directory.

A guide through our contributions

The core definitions of (semi)linear maps, equivalences, etc. are in algebra.module.linear_map and data.equiv.module.
The type classes ring_hom_comp_triple and ring_hom_inv_pair needed for composition and inversion of semilinear maps appear in algebra.ring.comp_typeclasses, as do most of the “universal” instances of these type classes. The instance star_ring_end.ring_hom_inv_pair needed for composition of conjugate-linear maps appears in algebra.star.basic (the rest of that file was written by other authors).
A test file checks the behavior of the conjugate-linear map notation and type classes.
Some files which required particular attention during the refactor to semilinear maps were linear_algebra.basic, topology.algebra.module.basic, analysis.normed_space.linear_isometry, and analysis.normed_space.operator_norm.
The is_R_or_C type class is defined in data.complex.is_R_or_C.
The Fréchet-Riesz representation theorem (inner_product_space.to_dual) is defined in analysis.inner_product_space.dual.
The adjoint (continuous_linear_map.adjoint) is defined in analysis.inner_product_space.adjoint, as is its finite-dimensional specialization (linear_map.adjoint). The definitions of self-adjoint and normal operators (self_adjoint, is_star_normal) are in algebra.star.self_adjoint; these definitions are made in the more abstract context of a star_ring. The “implementation detail” inner_product_space.is_normal is defined in analysis.inner_product_space.basic (the file as a whole has many authors).
\(\ell^p\) spaces are defined in analysis.normed_space.lp_space. The Hilbert sum of a family of inner product spaces is found in analysis.inner_product_space.l2_space.
Both the finite- and infinite-dimensional versions of the spectral theorem are in analysis.inner_product_space.spectrum, with many preliminaries in analysis.inner_product_space.rayleigh. Preliminaries about compact operators can be found in analysis.normed_space.compact_map.
The definition and classification of isocrystals can be found in ring_theory.witt_vector.isocrystal. The construction of the “Frobenius rotation,” the key lemma of the classification theorem, is done in ring_theory.witt_vector.is_alg_closed with preliminary work in ring_theory.witt_vector.mul_coeff. Preliminary work to show that the Witt vectors over a domain are a domain is done in ring_theory.witt_vector.domain.

Important pull requests

Much of our work has already been merged into mathlib. We list some of the primary pull requests here for reference. This is far from a complete list of the PRs connected to this paper.