TraceSeparableAdjoin.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Adjoining one element preserves trace separability

Separate continuity of multiplication in the tracial two-norm makes the two-norm closure of a star algebra another star algebra. A countable approximation to the base then suffices for its algebraic extension by one element.

theorem OAI.KadisonKastler.TraceSeparable.mono line 24
Source documentation
Trace separability passes to every subset.
```
theorem TraceSeparable.mono {τ : FaithfulTracialState B} {S T : Set B}
    (hS : TraceSeparable τ S) (hTS : T ⊆ S) : TraceSeparable τ T := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceSeparable

theorem OAI.KadisonKastler.TraceSeparable.map line 61

Source documentation

A trace-preserving star homomorphism preserves two-norm separability.

theorem TraceSeparable.map {C : Type*} [CStarAlgebra C]
    {τ : FaithfulTracialState B} {σ : FaithfulTracialState C} {S : Set B}
    (hS : TraceSeparable τ S) (φ : B →⋆ₐ[ℂ] C)
    (hφ : ∀ x, σ.toLinearMap (φ x) = τ.toLinearMap x) :
    TraceSeparable σ (φ '' S) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceSeparable

def OAI.KadisonKastler.traceClosure line 77
Source documentation
The algebra of all two-norm limits of elements of a star subalgebra.
```
def traceClosure (τ : FaithfulTracialState B) (A : StarSubalgebra ℂ B) :
    StarSubalgebra ℂ B where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.le_traceClosure line 119
Source documentation
Every element of the original algebra is in its two-norm closure.
```
theorem le_traceClosure (τ : FaithfulTracialState B) (A : StarSubalgebra ℂ B) :
    A ≤ traceClosure τ A := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceClosure
theorem OAI.KadisonKastler.TraceSeparable.adjoin_singleton line 126
Source documentation
Adjoining one element to a trace-separable algebra preserves trace separability. The adjoined element need not be unitary.
```
theorem TraceSeparable.adjoin_singleton (τ : FaithfulTracialState B)
    (A : StarSubalgebra ℂ B) (hA : TraceSeparable τ (A : Set B)) (u : B) :
    TraceSeparable τ (StarAlgebra.adjoin ℂ ((A : Set B) ∪ {u}) : Set B) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceSeparable