PublishedSimpleDerivation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Sakai's inner-derivation theorem, in its needed unital form

S. Sakai, Derivations of simple C-algebras II*, Bulletin de la Société Mathématique de France 99 (1971), 259--263, §2, unnumbered theorem on p.260, together with the unital specialization explained in §1 on p.259. DOI: 10.24033/bsmf.1719. The only input is innerness of bounded derivations of a simple unital C-star algebra. Self-adjointness of an implementer is derived below, not included in that input.

def OAI.KadisonKastler.CStarSimple line 25
Source documentation
Simplicity in the C-star sense: there are no proper nonzero closed two-sided ideals. Nontriviality is supplied separately where used.
```
def CStarSimple (A : Type*) [CStarAlgebra A] : Prop :=
…
```
def OAI.KadisonKastler.PublishedSimpleDerivationInner line 29
Source documentation
The published theorem, with no separability assumption.
```
def PublishedSimpleDerivationInner : Prop :=
…
```

theorem OAI.KadisonKastler.selfAdjoint_inner_implementer line 39

Source documentation

A commutator with a self-adjoint ambient element is anti-star compatible. Taking the real part of any inner implementer preserves it.

theorem selfAdjoint_inner_implementer (D : A →L[ℂ] A)
    (hstar : ∀ x, D (star x) = -star (D x))
    {a : A} (ha : ∀ x, D x = a * x - x * a) :
    ∃ b : A, IsSelfAdjoint b ∧ ∀ x, D x = b * x - x * b := by
…

theorem OAI.KadisonKastler.exists_selfAdjoint_implementer_of_published line 64