Normalizer.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Published small-normalizer factorization and its consequence

The factorization hypothesis is Proposition 3.2 of Cameron–Christensen–Sinclair–Smith–White–Wiggins, Kadison–Kastler stable factors, Duke Math. J. 163 (2014), 2639–2686. That proposition factors two sufficiently close normalizers through the algebra and its commutant.

Its specialization at the identity gives the small exact normalizer lemma used in §7 of Universal strong Kadison–Kastler stability (2026), with radius one and displacement constant four, under the stated factorization hypothesis.

theorem OAI.KadisonKastler.commute_of_mem_algebra_mem_commutant line 28

Source documentation

A unitary in an algebra commutes with a unitary in its commutant.

theorem commute_of_mem_algebra_mem_commutant {P : VonNeumannAlgebra H}
    {a b : unitary (H →L[ℂ] H)} (ha : (a : H →L[ℂ] H) ∈ P)
    (hb : (b : H →L[ℂ] H) ∈ P.commutant) :
    Commute (a : H →L[ℂ] H) (b : H →L[ℂ] H) :=
…

theorem OAI.KadisonKastler.conjugates_self_of_mem line 35
Source documentation
Unitaries belonging to the algebra normalize it.
```
theorem conjugates_self_of_mem {P : VonNeumannAlgebra H}
    {a : unitary (H →L[ℂ] H)} (ha : (a : H →L[ℂ] H) ∈ P) :
    Conjugates a P P := by
…
```
Mentions: OAI.KadisonKastler.Conjugates

theorem OAI.KadisonKastler.unitaryConj_eq_self_of_mem_commutant line 50

Source documentation

Unitaries in the commutant act trivially on the algebra by conjugation.

theorem unitaryConj_eq_self_of_mem_commutant {P : VonNeumannAlgebra H}
    {b : unitary (H →L[ℂ] H)} (hb : (b : H →L[ℂ] H) ∈ P.commutant)
    {x : H →L[ℂ] H} (hx : x ∈ P) : unitaryConj b x = x := by
…

Mentions: OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.conjugates_self_of_mem_commutant line 57

theorem OAI.KadisonKastler.conjugates_self_of_separate_factors line 69

Source documentation

A product of an algebra unitary and a commutant unitary normalizes the algebra.

theorem conjugates_self_of_separate_factors {P : VonNeumannAlgebra H}
    {a b : unitary (H →L[ℂ] H)} (ha : (a : H →L[ℂ] H) ∈ P)
    (hb : (b : H →L[ℂ] H) ∈ P.commutant) : Conjugates (a * b) P P :=
…

Mentions: OAI.KadisonKastler.Conjugates

def OAI.KadisonKastler.PublishedNormalizerFactorization line 76
Source documentation
Precisely the quantitative normalizer factorization of CCSSWW (2014), Proposition 3.2. Distances are written in the symmetric order u₂ - u₁.
```
def PublishedNormalizerFactorization : Prop :=
…
```
theorem OAI.KadisonKastler.small_exact_normalizer line 90
Source documentation
The small exact normalizer consequence of the published factorization. Unlike the application in the manuscript, this input already applies to arbitrary von Neumann algebras.
```
theorem small_exact_normalizer
    (hPublished : PublishedNormalizerFactorization (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedNormalizerFactorization