A nonzero abelian projection yields a homogeneous type I central piece
ProvedOAI.BoundedHochschild.KadisonRingrose.exists_homogeneous_piece_of_abelian_traceThroughout, is a unital C*-algebra with a partial order making it star-ordered, is a complex Banach space, and is an isometric conjugate-linear isomorphism, so is a von Neumann algebra with predual (the Lean hypothesis e). Let be a positive functional on that is tracial and faithful, and let be an abelian projection. Then there is a nonzero central projection whose corner is homogeneous of type I (HomogeneousTypeICorner z): for some the corner has a matrix system of size with one abelian diagonal unit.
Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.
import Mathlib
import Definitions.Def_KadisonRingroseSupport2
namespace OAI
noncomputable section
open scoped ComplexOrder
namespace BoundedHochschild.KadisonRingrose
open HochschildCorners FinitePathMain
universe u
variable {M X : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
[NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
theorem exists_homogeneous_piece_of_abelian_trace
(e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (τ : M →ₚ[ℂ] ℂ)
(htr : ∀ a b : M, τ (a * b) = τ (b * a))
(hfaith : ∀ a : M, τ (star a * a) = 0 → a = 0)
{p : M} (hp : AbelianProjection p) (hp0 : p ≠ 0) :
∃ z : M, CentralProjection z ∧ z ≠ 0 ∧ HomogeneousTypeICorner z := by
sorry
end BoundedHochschild.KadisonRingrose
end
end OAI