SeparableCenterInjectivity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of separably acting commutative algebras

Compress the countable amplification to the faithful cyclic space, apply the abelian unitary average, then use the inverse star isomorphism. This is the center-injectivity specialization used by the separable reduction in the universal stability theorem.

theorem OAI.KadisonKastler.faithfulCyclicHom_eq_compression line 28
theorem OAI.KadisonKastler.isInjective_of_commutative_separable line 39
theorem OAI.KadisonKastler.publishedCenterInjectivity_separable line 75
Source documentation
Blackadar's center-injectivity input, specialized to the separable representations in which the center-alignment reduction uses it.
```
theorem publishedCenterInjectivity_separable : PublishedCenterInjectivity (H := H) := by
…
```
Mentions: OAI.KadisonKastler.PublishedCenterInjectivity