TypeIInjectivity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of type I factors in their given representation

The cyclic restriction at a minimal projection is faithful and irreducible. Kaplansky approximation and weak compactness of the original operator ball make it surjective onto all operators on that cyclic space. Compression, followed by the inverse restriction, is therefore an ambient contractive projection onto the original algebra.

theorem OAI.KadisonKastler.typeICyclicHom_bicommutant line 27
theorem OAI.KadisonKastler.typeICyclicHom_surjective_unitBall line 39
Source documentation
Every operator on the minimal cyclic space comes from the original factor; the assertion includes the closed unit ball without norm loss.
```
theorem typeICyclicHom_surjective_unitBall (hM : ScalarCenter M)
    (p : AlgebraProjection M) (hp : IsMinimalProjectionIn M p)
    (ξ : H) (hξ : ξ ≠ 0) (hpξ : p.val.val ξ = ξ)
    (T : typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ) (hT : ‖T‖ ≤ 1) :
    ∃ a : Algebra M, ‖a‖ ≤ 1 ∧ typeICyclicHom ξ a = T := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.typeICyclicHom
theorem OAI.KadisonKastler.typeICyclicHom_surjective line 84
def OAI.KadisonKastler.typeICyclicEquiv line 108
Source documentation
The algebraic identification with all operators on the minimal cyclic space, constructed in the original representation.
```
def typeICyclicEquiv (hM : ScalarCenter M) (p : AlgebraProjection M)
    (hp : IsMinimalProjectionIn M p) (ξ : H) (hξ : ξ ≠ 0)
    (hpξ : p.val.val ξ = ξ) :
    Algebra M ≃⋆ₐ[ℂ] (typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ) :=
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.typeICyclicSpace
theorem OAI.KadisonKastler.typeICyclicHom_eq_compression line 116
theorem OAI.KadisonKastler.IsTypeIFactor.isInjective line 126
Source documentation
Compression to the minimal cyclic space, transported back to the original factor, is a contractive projection of the ambient operators.
```
theorem IsTypeIFactor.isInjective (hM : IsTypeIFactor M) : IsInjective M := by
…
```
Mentions: OAI.KadisonKastler.IsTypeIFactor, OAI.KadisonKastler.IsInjective
theorem OAI.KadisonKastler.publishedTypeIInjectivity line 158
Source documentation
The type I injectivity input is an unconditional theorem.
```
theorem publishedTypeIInjectivity : PublishedTypeIInjectivity (H := H) := by
…
```
Mentions: OAI.KadisonKastler.PublishedTypeIInjectivity