English
An idempotent e belongs to S if and only if, for every y in S.commutant, range e lies in invtSubmodule y and ker e lies in invtSubmodule y.
Русский
Элемент e, удовлетворяющий e^2 = e, принадлежит S тогда и только тогда, когда для каждого y ∈ S.commutant образ e и ядро e лежат в invtSubmodule y.
LaTeX
$$$e \\in S \\iff \\forall y \\in S.commutant,\\; \\mathrm{range}(e) \\in \\mathrm{InvtSubmodule}(y) \\land \\mathrm{ker}(e) \\in \\mathrm{InvtSubmodule}(y).$$$
Lean4
/-- A star projection is an element in a von Neumann algebra if and only if
its range is invariant under the commutant. -/
theorem mem_iff {e : H →L[ℂ] H} (he : IsStarProjection e) (S : VonNeumannAlgebra H) :
e ∈ S ↔ ∀ y ∈ S.commutant, LinearMap.range e ∈ Module.End.invtSubmodule y :=
by
simp_rw [he.isIdempotentElem.mem_iff, he.isIdempotentElem.range_mem_invtSubmodule_iff,
he.isIdempotentElem.ker_mem_invtSubmodule_iff, forall_and, and_iff_left_iff_imp, ← mul_def]
intro h x hx
simpa [he.isSelfAdjoint.star_eq] using congr(star $(h _ (star_mem hx)))
