UnitaryLifts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Unitary lifts through quotients of finite-factor sequence algebras

The concrete finite-factor polar decomposition extends to a unitary. Applying it coordinatewise, continuous functional calculus shows that a unitary quotient class has a bounded sequence of unitary representatives.

theorem OAI.KadisonKastler.exists_unitary_polar line 30
Source documentation
Coordinatewise unitary polar decomposition in the concrete factor.
```
theorem exists_unitary_polar (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (x : Algebra M) : ∃ v : unitary (Algebra M), (v : Algebra M) * CFC.abs x = x := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.exists_unitary_sequence_lift line 40
Source documentation
A unitary in a quotient of the bounded sequences has actual unitary coordinate representatives. Surjectivity and finite polar decomposition suffice; there is no norm or trace approximation premise.
```
theorem exists_unitary_sequence_lift (hM : Generator.IsII1Factor M.toStarSubalgebra)
    {Q : Type*} [CStarAlgebra Q]
    (π : BoundedSequence (Algebra M) →⋆ₐ[ℂ] Q) (hπ : Function.Surjective π)
    (u : unitary Q) :
    ∃ v : unitary (BoundedSequence (Algebra M)), π (v : BoundedSequence (Algebra M)) = u := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TracialUltrapower.unitary_lift line 75
Source documentation
The standard represented tracial ultrapower admits unitary lifts.
```
theorem TracialUltrapower.unitary_lift
    {hM : Generator.IsII1Factor M.toStarSubalgebra} {ω : Ultrafilter ℕ}
    (Q : TracialUltrapower (concreteFactorTrace hM) ω) (u : unitary (Algebra Q.algebra)) :
    ∃ v : unitary (BoundedSequence (Algebra M)), Q.quotient v = u :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.TracialUltrapower, OAI.KadisonKastler.concreteFactorTrace, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedSequence