TraceFreeProjectionJoins.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Projection joins before trace existence

The join of two projections is obtained by adding the range projection of (1 - p) * q to p. Polar decomposition also embeds the added projection into q. This is the projection comparison used in Ringrose's Lemma 5.2.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_trace_free_projection_join line 27

Source documentation

A trace-free join, with the part added to p equivalent to a subprojection of q. The formula records the partial isometry needed in finite joins.

theorem exists_trace_free_projection_join (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (p q : M) (hp : IsStarProjection p) (hq : IsStarProjection q) :
    ∃ v : PartialIso M, v.initial ≤ q ∧ p * v.final = 0 ∧
      IsStarProjection (p + v.final) ∧ p ≤ p + v.final ∧ q ≤ p + v.final ∧
      ∀ z : M, IsStarProjection z → p ≤ z → q ≤ z → p + v.final ≤ z := by
…