TypeICentralSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Central type I support without a trace

The maximal central projection annihilating an abelian projection exists by weak-star compactness. Its complement is a nonzero central type I support. The construction applies to every von Neumann algebra and requires no faithful tracial state.

lemma OAI.BoundedHochschild.KadisonRingrose.central_annihilator_chain line 27

Source documentation

A chain of central projections annihilating one element has a central projection upper bound that still annihilates it.

lemma central_annihilator_chain (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (p : M) (c : Set M) (hc : IsChain (· ≤ ·) c) (hne : c.Nonempty)
    (hs : ∀ q ∈ c, CentralProjection q ∧ q * p = 0) :
    ∃ s : M, CentralProjection s ∧ s * p = 0 ∧ ∀ q ∈ c, q ≤ s := by
…

theorem OAI.BoundedHochschild.KadisonRingrose.exists_typeI_support line 37

Source documentation

Every nonzero abelian projection has a nonzero central type I support.

theorem exists_typeI_support (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (hp : AbelianProjection p) (hp0 : p ≠ 0) :
    ∃ z : M, TypeICentralSummand z ∧ p ≤ z ∧ z ≠ 0 := by
…