Papers With

← All papers
First page of Wickstead's conjecture on positive projections and non-representable Banach lattice algebras

Wickstead's conjecture on positive projections and non-representable Banach lattice algebras

David Muñoz-Lahoz

math.FA Apr 16, 2026 · v3 math.OA
formalization analysis mathlib
Read PDF arXiv abstract Code
TL;DR
Main results, including Wickstead's conjecture, are formalized in Lean 4 using the banlat Banach lattice library built on Mathlib.
Abstract
Let $X$ be a Dedekind complete Banach lattice, and let $P\colon X\to X$ be a positive projection for which the largest central operator below $P$ is $α\operatorname{id}_X$, for some $α\ge 0$. Wickstead conjectured that $α$ must either be $0$ or $1/n$, for some $n \in \mathbb{N}$, and proved it for finite-dimensional $X$. In this paper, we show that the conjecture holds in general. As a consequence, we settle the representation problem for Banach lattice algebras: we show that there exist Banach lattice algebras of dimension $2$ that do not admit a faithful representation as regular operators on any Dedekind complete Banach lattice. All the main results in this paper have been formalized in Lean 4 using the Banach lattice Lean library.
Problem

Wickstead conjectured that if a positive projection P on a Dedekind complete Banach lattice has constant diagonal α (the largest central operator below P is α·id), then α is 0 or 1/n for some natural number n. He proved this only for finite-dimensional spaces. The question bears on whether every Banach lattice algebra can be faithfully represented as regular operators on a Dedekind complete Banach lattice.

Approach

The case of C(K) spaces is proved first: for a unital positive projection with constant diagonal α, α is either 0 or 1/n. The general case reduces to this one by restricting to the principal ideal generated by Pe and using Kakutani's representation theorem together with the Riesz–Kantorovich formulas. Lemmas on positive idempotents in L_r(X) then apply the result to construct a counterexample for the representation problem. The main results are formalized in Lean 4 using the banlat library v0.1.0 on Mathlib v4.30.0, with statements in the paper tagged by links to the repository.

Results

Wickstead's conjecture holds in full generality. There exist 2-dimensional Banach lattice algebras with no faithful representation as regular operators on any Dedekind complete Banach lattice, which settles the representation problem negatively.