Centralizers and conjugation by units

If conjugation by the inverse of a unit u maps a set S of a monoid into itself, then conjugation by u maps the centralizer of S into itself. Applying this twice shows that a double commutant is preserved by every unit whose conjugations preserve the original set in both directions, which is how spatially implemented automorphisms extend to von Neumann algebras.

theorem Set.conj_mem_centralizer {M : Type u_1} [Monoid M] {S : Set M} (u : Mˣ) (hS : ∀ s ∈ S, ↑u⁻¹ * s * ↑u ∈ S) {x : M} (hx : x ∈ S.centralizer) : ↑u * x * ↑u⁻¹ ∈ S.centralizer

Conjugation by a unit u maps the centralizer of S into itself when conjugation by u⁻¹ maps S into itself.