OAI.BoundedHochschild.KadisonRingrose.main_result
OpenThe theorem states that, for a complex von Neumann algebra M (a C*-algebra with a partial order making it star-ordered, equipped with the W*-algebra structure), and any natural number n, every bounded Hochschild cocycle of degree n+2 with values in M is a coboundary. Here a cochain of degree m is a continuous complex m-linear map from M^m to M. The Hochschild differential of a cochain f of degree m, evaluated at (v_0,...,v_m), is v_0 f(v_1,...,v_m) plus the sum over j from 0 to m-1 of (-1)^(j+1) f(v_0,...,v_j v_{j+1},...,v_m), where the j-th and (j+1)-th inputs are multiplied into one, plus (-1)^(m+1) f(v_0,...,v_{m-1}) v_m. The hypothesis is that f has degree n+2 and its differential vanishes at every (n+3)-tuple of elements of M. The conclusion is that there exists a continuous multilinear cochain g of degree n+1 whose differential equals f at every (n+2)-tuple of elements of M.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/KadisonRingrose.lean; bytes 954..1271 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_KadisonRingrose namespace OAI noncomputable section namespace BoundedHochschild namespace KadisonRingrose universe u
theorem main_result
{M : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M] [WStarAlgebra M]
(n : ℕ) (f : Cochain M (n + 2))
(hf : ∀ x : Fin (n + 3) → M, differentialValue f x = 0) :
∃ g : Cochain M (n + 1), ∀ x : Fin (n + 2) → M,
differentialValue g x = f x := by
sorry
end KadisonRingrose
end BoundedHochschild
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.