The normal projection preserves normal coefficients

Proved

OAI.HochschildNormalPart.normalProjection_fixes_normal

by wurtle · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

bounded-hochschild-cohomologyoai-math

Let $M$ be a unital C*-algebra with predual $X$ through an isometric conjugate-linear isomorphism $e:X^*\to M$ , and $\pi:M\to B(H)$ a unital *-homomorphism on a Hilbert space. For $\eta,\xi\in H$ let $\omega_{\eta,\xi}(a)=\langle\eta,\pi(a)\xi\rangle$ (coefficient π η ξ). Let $P$ be the orthogonal projection (normalProjection e π) onto the closed subspace of vectors $\xi$ for which $\omega_{\zeta,\xi}$ is normal for all $\zeta$ (normalVectors e π). If $\omega_{\eta,\xi}$ is normal, then

\omega_{\eta,P\xi}=\omega_{\eta,\xi}.

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.

Preamble

import Mathlib
import Definitions.Def_KadisonRingroseSupport2

namespace OAI

noncomputable section

open scoped ComplexOrder
open Filter Topology
open Filter Topology Metric
open Filter Topology MeasureTheory
open scoped RealInnerProductSpace ENNReal
open MeasureTheory ProbabilityTheory Filter Topology
open scoped ENNReal
open MeasureTheory ProbabilityTheory
open MeasureTheory Filter Topology
open scoped ComplexOrder BoundedContinuousFunction
open MeasureTheory Filter Topology TopologicalSpace
open scoped ENNReal Function
open scoped NNReal
open scoped ComplexOrder BoundedContinuousFunction CStarAlgebra
open scoped ComplexOrder CStarAlgebra
open scoped BigOperators
open scoped InnerProductSpace
namespace HochschildNormalPart
universe u v
variable {M X : Type u} [CStarAlgebra M]
  [NormedAddCommGroup X] [NormedSpace ℂ X]
  (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)

variable [CompleteSpace X]

variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : M →⋆ₐ[ℂ] (H →L[ℂ] H))

Formal statement

theorem normalProjection_fixes_normal (η ξ : H)
    (h : coefficient π η ξ ∈ normalDual e) :
    coefficient π η (normalProjection e π ξ)=coefficient π η ξ := by
  sorry

end HochschildNormalPart
end
end OAI

Source

OpenAI, Vanishing of higher bounded Hochschild cohomology, September 23, 2026, https://github.com/openai/math (paper: preprints/Vanishing-of-higher-bounded-Hochschild-cohomology-September-23-2026/paper.pdf; Apache License 2.0); Lean declaration `OAI.HochschildNormalPart.normalProjection_fixes_normal`, https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/BoundedHochschild/NormalVectors.lean#L269

View graph