TomiyamaField.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Tomiyama's bimodule identity for measurable operator fields

The measurable representative algebra has norm-dense projection span, by the pointwise spectral construction. This property descends through its quotient map. The projection identities for contractive retractions therefore give the field version of Tomiyama's theorem.

theorem OAI.KadisonKastler.weakOperatorField_closed_projection_span_eq_top line 25
Source documentation
Norm-density of projection spans passes to the field quotient.
```
theorem weakOperatorField_closed_projection_span_eq_top :
    (Submodule.span ℂ {p : WeakOperatorField (H := H) μ |
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.publishedFieldTomiyama line 39
Source documentation
The constant-field specialization of Tomiyama's theorem is proved from the C-star norm geometry and measurable spectral projections.
```
theorem publishedFieldTomiyama : PublishedFieldTomiyama (G := G) (H := H) (μ := μ) := by
…
```
Mentions: OAI.KadisonKastler.PublishedFieldTomiyama