PublishedCenterInjectivity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Published injectivity of the concrete center

Blackadar, Operator Algebras, Corollary IV.2.2.10, p. 377 (PDF p. 385), states that commutative von Neumann algebras are injective. Proposition IV.2.1.4(iii), p. 373, gives the norm-one projection in every faithful representation. Only centers in their given representation are retained.

Primary text: https://bruceblackadar.com/Mathematics/Cycr.pdf

def OAI.KadisonKastler.PublishedCenterInjectivity line 21
Source documentation
The represented-center specialization; no perturbation conclusion is assumed.
```
def PublishedCenterInjectivity : Prop :=
…
```