commutant — Mathlib

English

The centralizer (commutant) of S is the von Neumann algebra consisting of all operators that commute with every element of S.

Русский

Централизатор (коммутант) S — это алгебра Вона, состоящая из всех операторов, коммутирующих с каждым элементом S.

LaTeX

$$$S^{\\prime} := \\text{centralizer}(S) \\;\\text{is a von Neumann algebra on } H$$$

Lean4

/-- The centralizer of a `VonNeumannAlgebra`, as a `VonNeumannAlgebra`. -/
noncomputable def commutant (S : VonNeumannAlgebra H) : VonNeumannAlgebra H
    where
  toStarSubalgebra := StarSubalgebra.centralizer ℂ (S : Set (H →L[ℂ] H))
  centralizer_centralizer' := by simp

Похожие утверждения