Papers With

← All papers
First page of Order continuity of induced homomorphisms between free Banach lattices

Order continuity of induced homomorphisms between free Banach lattices

Raúl E. Pariente-Martín, Pedro Tradacete

math.FA Oct 30, 2026 · v1
formalization mathlib analysis
Read PDF arXiv abstract Code
TL;DR
All theorems, propositions, lemmas and corollaries are formalized in Lean 4 with Mathlib and the BanLat Banach lattice library, linked per statement.
Abstract
Let $T\colon F\to E$ be a bounded operator between Banach spaces and let $\overline T\colon FBL^{(p)}[F]\to FBL^{(p)}[E]$ be the lattice homomorphism induced by $T$ between the corresponding free $p$-convex Banach lattices generated by $F$ and $E$. We show that $\overline T$ is order continuous if and only if it is either zero or a lattice isomorphic embedding. For $p=\infty$, this holds precisely when $T$ is zero or an isomorphic embedding, while for $1\leq p<\infty$, apart from the zero operator, $T$ must be an embedding and the pair $(T(F),E)$ must have the operator-extension property POE-$p$. In addition, we study when $FBL^{(p)}[E]$ is order dense or majorizing in $FBL^{(q)}[E]$ for $p<q$.
Problem

Characterize when the lattice homomorphism induced by a bounded operator T between Banach spaces, acting between free p-convex Banach lattices, is order continuous. A related question is when FBL^(p)[E] is order dense or majorizing in FBL^(q)[E] for p<q.

Approach

Uses the functional representation of free p-convex Banach lattices as positively homogeneous functions on the dual space. Support functions of compact sets and an equivalent majorant form of the free p-convex norm are used to control norms. The operator-extension property POE-p is linked to order continuity. All results are formalized in Lean 4 with Mathlib and the BanLat library, and each statement is linked to its Lean declaration.

Results

The induced homomorphism is order continuous iff it is zero or a lattice isomorphic embedding. For p=∞ this happens iff T is zero or an isomorphic embedding; for p<∞ it additionally requires the pair (T(F),E) to have POE-p. For p<q, order continuity, surjectivity, majorizing range and order density of the canonical inclusion are equivalent to every q-compact disk lying inside a p-compact disk.