TypeIICharacterization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Type II structure without an assumed trace

A nonzero abelian projection has a central type I support, with the type I condition tested on all subprojections. Thus absence of a type I central part is equivalent to absence of abelian corners, before constructing a trace. The projection-halving theorem can consequently use exactly the type II hypothesis of the main application.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_typeICorner_support line 33

Source documentation

A nonzero abelian projection generates a nonzero central type I part.

theorem exists_typeICorner_support (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (hp : IsStarProjection p) (hpa : PopaTypeII.AbelianProjection hp)
    (hp0 : p ≠ 0) :
    ∃ (z : M) (hz : IsStarProjection z), (∀ a : M, z * a = a * z) ∧
      p ≤ z ∧ z ≠ 0 ∧ PopaTypeII.TypeICorner hz := by
…

Mentions: OAI.PopaTypeII.AbelianProjection, OAI.PopaTypeII.TypeICorner

theorem OAI.BoundedHochschild.KadisonRingrose.noTypeICentralPart_iff_noAbelianCorners line 94
Source documentation
The two type II hypotheses agree for every von Neumann algebra, without a faithful normal trace hypothesis.
```
theorem noTypeICentralPart_iff_noAbelianCorners (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    PopaTypeII.NoTypeICentralPart M ↔ PopaTypeII.NoAbelianCorners M := by
…
```
Mentions: OAI.PopaTypeII.NoTypeICentralPart, OAI.PopaTypeII.NoAbelianCorners

theorem OAI.BoundedHochschild.KadisonRingrose.typeII_projection_halving line 109

Source documentation

Exact type II projection halving, before the finite trace is constructed.

theorem typeII_projection_halving (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hII : PopaTypeII.NoTypeICentralPart M) {p : M} (hp : IsStarProjection p) :
    ∃ v : PartialIso M, v.initial * v.final = 0 ∧ v.initial + v.final = p :=
…

Mentions: OAI.PopaTypeII.NoTypeICentralPart