TomiyamaBimodule.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bimodule identities for projections

The opposite-corner norm comparison completes the algebraic part of Tomiyama's theorem. The last theorem extends the identities whenever the target is the norm closure of the span of its projections.

theorem OAI.KadisonKastler.tomiyama_no_reverse_block line 22

theorem OAI.KadisonKastler.tomiyama_offDiagonal line 65

Source documentation

Retractions preserve the orientation of off-diagonal blocks.

theorem tomiyama_offDiagonal (e : B) (he : IsStarProjection e)
    (z : A) (hel : φ e * z = z) (her : z * φ e = 0) :
    P z = e * P z * (1 - e) := by
…

theorem OAI.KadisonKastler.tomiyama_map_projection_mul line 80
Source documentation
Left multiplication by any projection in the target commutes with the contractive retraction.
```
theorem tomiyama_map_projection_mul (e : B) (he : IsStarProjection e) (x : A) :
    P (φ e * x) = e * P x := by
…
```
theorem OAI.KadisonKastler.tomiyama_map_mul_projection line 137
Source documentation
The right identity follows by taking adjoints.
```
theorem tomiyama_map_mul_projection (e : B) (he : IsStarProjection e) (x : A) :
    P (x * φ e) = P x * e := by
…
```