BoundaryFiniteIsomorphism.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

From a normalized boundary field to a finite-factor isomorphism

This joins the measurable simultaneous-point argument to the algebraic unitary-image construction. The boundary comparison unitaries are required to take values in the neighboring algebra, as supplied by the restricted operator-field mean and the diagonal trace construction.

def OAI.KadisonKastler.algebraVectorMap line 23
Source documentation
Evaluating the represented algebra at its trace vector.
```
def algebraVectorMap (M : VonNeumannAlgebra H) (Ω : H) : Algebra M →ₗ[ℂ] H where
…
```
Mentions: OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.ambientAlgebraUnitary line 29
Source documentation
The unitary in the ambient operator algebra.
```
def ambientAlgebraUnitary {M : VonNeumannAlgebra H} (u : unitary (Algebra M)) :
    unitary (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.algebraUnitaryOfMem line 34
Source documentation
A unitary with value in the algebra is a unitary of that algebra.
```
def algebraUnitaryOfMem {M : VonNeumannAlgebra H} (u : unitary (H →L[ℂ] H))
    (hu : (u : H →L[ℂ] H) ∈ M) : unitary (Algebra M) :=
…
```
Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_starEquiv_of_boundary_normalization line 49

Source documentation

Once the scalar boundary relation has been obtained, the actual algebra-valued comparison fields yield a nearby star isomorphism.

theorem exists_starEquiv_of_boundary_normalization
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (hτM : FiniteVectorTrace τM) (hτN : FiniteVectorTrace τN)
    (Ω : H)
    (hMΩ : ∀ a, ‖algebraVectorMap M Ω a‖ = traceTwoNorm τM a)
    (hNΩ : ∀ a, ‖algebraVectorMap N Ω a‖ = traceTwoNorm τN a)
    (ρ : G → unitary (Algebra M))
    (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
      ∃ g, traceTwoNorm τM ((u : Algebra M) - ρ g) < ε)
    (α : NonsingularAction G D μ)
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.NonsingularAction