Absorption.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Cuntz-algebra absorption

Absorption is expressed by a star-algebra isomorphism with the minimal tensor product. The implication from nuclear strong pure infiniteness is the specialization to O∞ of E. Kirchberg, Central sequences in C-algebras and strongly purely infinite algebras*, in Operator Algebras: The Abel Symposium 2004 (2006), pp. 175--231, Proposition 4.4(4),(5) and Remark 4.6, together with the central-sequence embedding preceding Proposition 4.4.

For a possibly nonunital separable algebra, the unital central embedding is into (Aω ∩ A') / Ann(A, Aω). The zero algebra is included.

Source: https://abelsymposium.no/symp2004/preprints/kirchberg.pdf.

def OAI.WeakPureInfiniteness.AbsorbsOInfinity line 27
Source documentation
Absorption of the Cuntz algebra, expressed by a star-algebra isomorphism.
```
def AbsorbsOInfinity (A : Type u) [NonUnitalCStarAlgebra A] : Prop :=
…
```
def OAI.WeakPureInfiniteness.KirchbergOInfinityAbsorption line 35
Source documentation
Nuclear strong pure infiniteness implies absorption for a separable algebra, including the zero algebra, without a unit or simplicity hypothesis.
```
def KirchbergOInfinityAbsorption [TopologicalSpace.SeparableSpace A] : Prop :=
…
```
theorem OAI.WeakPureInfiniteness.oInfinityTensor_subsingleton line 40
Source documentation
A zero algebra has a zero minimal tensor product with OInfinity.
```
theorem oInfinityTensor_subsingleton [Subsingleton A] :
    Subsingleton (MinimalTensor A OInfinity) := by
…
```
Mentions: OAI.WeakPureInfiniteness.MinimalTensor, OAI.WeakPureInfiniteness.OInfinity
def OAI.WeakPureInfiniteness.starEquivOfSubsingleton line 58
theorem OAI.WeakPureInfiniteness.absorbsOInfinity_of_subsingleton line 72
Source documentation
The zero-algebra absorption isomorphism needs no nuclearity premise.
```
theorem absorbsOInfinity_of_subsingleton [Subsingleton A] : AbsorbsOInfinity A := by
…
```
Mentions: OAI.WeakPureInfiniteness.AbsorbsOInfinity
theorem OAI.WeakPureInfiniteness.kirchbergOInfinityAbsorption_of_subsingleton line 78
Source documentation
The published absorption input is discharged for the zero algebra.
```
theorem kirchbergOInfinityAbsorption_of_subsingleton
    [TopologicalSpace.SeparableSpace A] [Subsingleton A] :
    KirchbergOInfinityAbsorption A := by
…
```
Mentions: OAI.WeakPureInfiniteness.KirchbergOInfinityAbsorption