OAI/Analysis/BoundedHochschild/TraceFreeSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Central separation without a trace

A maximal projection annihilating the right ideal generated by a projection is central. Any off-diagonal block would have a nonzero support projection orthogonal to that maximal projection and permit an extension.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.exists_trace_free_central_separator line 26

    Source documentation

    Projections with zero intervening products admit a central separator.

    theorem exists_trace_free_central_separator (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p q : M} (hp : IsStarProjection p) (_hq : IsStarProjection q)
    (hpq : ∀ a : M, p * a * q = 0) :
    ∃ z : M, CentralProjection z ∧ p ≤ z ∧ z * q = 0 := by
…