VaryingUnitaryLifts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Unitary lifts in a varying finite product

Coordinate unitary polar decompositions produce an exact unitary lift through any surjective star quotient of the bounded product.

def OAI.KadisonKastler.varyingUnitarySequence line 41
Source documentation
A family of coordinate unitaries is bounded in the actual product.
```
def varyingUnitarySequence (v : ∀ j, unitary (B j)) :
    unitary (VaryingBoundedSequence B) := by
…
```
Mentions: OAI.KadisonKastler.VaryingBoundedSequence
theorem OAI.KadisonKastler.varyingUnitarySequence_apply line 52

theorem OAI.KadisonKastler.exists_varying_unitary_lift line 59

Source documentation

Coordinate polar decompositions suffice for unitary quotient lifting; no trace approximation or additional lifting axiom is needed.

theorem exists_varying_unitary_lift
    (hpolar : ∀ j (x : B j), ∃ v : unitary (B j), (v : B j) * CFC.abs x = x)
    (π : VaryingBoundedSequence B →⋆ₐ[ℂ] C) (hπ : Function.Surjective π)
    (u : unitary C) :
    ∃ v : unitary (VaryingBoundedSequence B), π (v : VaryingBoundedSequence B) = (u : C) := by
…

Mentions: OAI.KadisonKastler.VaryingBoundedSequence