OAI/Analysis/BoundedHochschild/MaximalInfiniteProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A maximal properly infinite projection has finite complement.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.projection_mul_zero_of_bounds line 18
  2. theorem OAI.BoundedHochschild.KadisonRingrose.exists_properlyInfinite_with_finite_complement line 30

    Source documentation

    A von Neumann algebra contains a properly infinite projection with finite complement. This includes the zero projection when the algebra is finite.

    theorem exists_properlyInfinite_with_finite_complement (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    ∃ p : M, IsStarProjection p ∧ ProperlyInfiniteProjection p ∧ FiniteCorner (1 - p) := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.ProperlyInfiniteProjection, OAI.BoundedHochschild.KadisonRingrose.FiniteCorner