DerivationExtensionFactor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Factoriality in Sakai's one-implementer extension

In an irreducible representation of the algebra generated by the source and its self-adjoint spatial implementer, every central projection of the source bicommutant commutes with all generators. It is therefore trivial.

def OAI.KadisonKastler.NormGeneratedExtension line 26
Source documentation
The norm-closed unital star algebra generated by the source and one element.
```
def NormGeneratedExtension (φ : A →⋆ₐ[ℂ] B) (d : B) : Prop :=
…
```
theorem OAI.KadisonKastler.commutes_of_normGeneratedExtension line 30
theorem OAI.KadisonKastler.factor_of_irreducible_derivation_extension line 55