OAI/Analysis/KadisonKastler/NormalizerTopology.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The closed group of unitary normalizers

Uniform limits of normalizing unitary families remain normalizing. This provides the complete space in which the normalizer correction is iterated.

  1. def OAI.KadisonKastler.normalizerGroup line 22

    Source documentation

    The normalizers of a concrete von Neumann algebra as an actual subgroup.

    def normalizerGroup (P : VonNeumannAlgebra H) : Subgroup (unitary (H →L[ℂ] H)) where
…
  2. theorem OAI.KadisonKastler.mem_normalizerGroup_iff line 30
  3. theorem OAI.KadisonKastler.isClosed_normalizerGroup line 50
  4. def OAI.KadisonKastler.NormalizingFamily line 72

    Source documentation

    Uniformly bounded families all of whose values normalize the algebra.

    def NormalizingFamily (P : VonNeumannAlgebra H) :=
…
  5. theorem OAI.KadisonKastler.continuous_unitaryFamilyEval line 76
  6. theorem OAI.KadisonKastler.isClosed_normalizingFamilies line 83
  7. instance OAI.KadisonKastler.normalizingFamilyMetricSpace line 90
  8. instance OAI.KadisonKastler.normalizingFamilyCompleteSpace line 93