On the extension of inner derivations from dense ideals in Banach algebras
Hamid Shafieasl, Amir Mohammad Tavakkoli
math.FA
Mar 10, 2026 · v1
TL;DR
Formally verifies in the Lean theorem prover a negative answer on extending inner derivations in Banach algebras.
Abstract
Let $A$ be a Banach algebra and $I$ a dense ideal in $A$. A natural question in the theory of operator algebras is whether the property that all derivations $D: A \to I$ are inner (implemented by elements in $I$) implies that all derivations $D: A \to A$ are inner (implemented by elements in $A$). We present a rigorous negative answer to this question. By utilizing the algebra of compact operators $A = K(H)$ and the dense ideal of finite-rank operators $I = F(H)$ on a separable infinite-dimensional Hilbert space $H$, we demonstrate that while every derivation into $F(H)$ is inner, there exist outer derivations on $K(H)$. Furthermore, we generalize this result to Schatten $p$-classes and discuss the cohomological implications and the role of approximate identities. Moreover, the main results and counterexamples presented in this paper have been formally verified using the Lean theorem prover.
Problem
Given a Banach algebra A and a dense ideal I, it is natural to ask whether the property that all derivations D: A -> I are inner (implemented by elements of I) implies all derivations D: A -> A are inner (implemented by elements of A).
Approach
The authors construct a counterexample using the algebra of compact operators K(H) and the dense ideal of finite-rank operators F(H) on a separable infinite-dimensional Hilbert space H. They show every derivation into F(H) is inner but exhibit derivations into K(H) that are not inner. The results are formally verified using the Lean theorem prover. The analysis extends to Schatten p-classes and examines the role of bounded approximate identities.
Results
The answer to the extension question is negative: innerness of derivations from A into a dense ideal I does not imply innerness of derivations from A into A. The obstruction generalizes to all Schatten p-class ideals S_p(H) for 1 <= p < infinity. The main results and counterexamples are formally verified in Lean.
