English
A formal identity relating the commutant of a commutant through a centralizer construction; expresses an equivalence of commutant constructions.
Русский
Формальная идентичность, связывающая коммутант коммутатора через конструкцию центрального центра; эквивалентность конструктов коммутанта.
LaTeX
$$$S^{\\prime} = \\text{centralizer}(\\text{Set.unite}(S))$$$
Lean4
/-- An idempotent is an element in a von Neumann algebra if and only if
its range and kernel are invariant under the commutant. -/
theorem mem_iff {e : H →L[ℂ] H} (h : IsIdempotentElem e) (S : VonNeumannAlgebra H) :
e ∈ S ↔
∀ y ∈ S.commutant,
LinearMap.range e ∈ Module.End.invtSubmodule y ∧ LinearMap.ker e ∈ Module.End.invtSubmodule y :=
by conv_rhs => simp [← h.commute_iff, Commute.symm_iff (a := e), commute_iff_eq, ← mem_commutant_iff]
