Vanishing of the projection defect for a factorized map
ProvedOAI.BoundedHochschild.KadisonRingrose.projection_defect_eq_zeroThroughout, 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 the normal GNS representation on NormalGNS e, let be a unital *-homomorphism on a Hilbert space, and let be bounded with for a bounded linear . Suppose for every projection . Then for all and every projection ,
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
namespace BoundedHochschild.KadisonRingrose
universe u
variable {M X : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
[NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
{K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
theorem projection_defect_eq_zero (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
(π : M →⋆ₐ[ℂ] (K →L[ℂ] K)) (L W : NormalGNS e →L[ℂ] K)
(T : M →L[ℂ] M)
(hT : ∀ a, normalGNSRepresentation e (T a) = L.adjoint.comp ((π a).comp W))
(hnorm : ∀ f : M, IsStarProjection f →
‖W.comp (normalGNSRepresentation e f)‖ =
‖(π f).comp (W.comp (normalGNSRepresentation e f))‖)
(a : M) {p : M} (hp : IsStarProjection p) : T a * p - T (a * p) * p = 0 := by
sorry
end BoundedHochschild.KadisonRingrose
end
end OAI