NormalRepresentationRange.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Ranges of faithful representations continuous on bounded weak nets

Kaplansky approximation and compactness of the source operator ball show that the range is already a von Neumann algebra. The same approximation transports a specified generating algebra into a target von Neumann algebra.

def OAI.KadisonKastler.BoundedWeakNormal line 24
theorem OAI.KadisonKastler.boundedWeakNormal_maps_generated line 32
theorem OAI.KadisonKastler.boundedWeakNormal_surjective_unitBall line 63
theorem OAI.KadisonKastler.boundedWeakNormal_surjective_generated line 95
def OAI.KadisonKastler.boundedWeakNormalEquiv line 115
Source documentation
A faithful representation continuous on bounded weak nets identifies the original algebra with its generated von Neumann algebra.
```
def boundedWeakNormalEquiv
    (M : VonNeumannAlgebra H) (φ : Algebra M →⋆ₐ[ℂ] (K →L[ℂ] K))
    (hfaith : Function.Injective φ) (hφ : BoundedWeakNormal M φ) :
    Algebra M ≃⋆ₐ[ℂ] Algebra (generatedVonNeumannAlgebra φ.range) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedWeakNormal, OAI.KadisonKastler.generatedVonNeumannAlgebra
def OAI.KadisonKastler.vonNeumannAlgebraEquivOfEq line 130