CentralSequenceAbsorption.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Absorption from the published central-sequence embedding

The embedding below is into (Aω ∩ A') / Ann(A, Aω). This is the central-sequence embedding immediately preceding Proposition 4.4 in Kirchberg, Central sequences in C-algebras and strongly purely infinite algebras*, Abel Symposia 1 (2006), 175--231. The structural hypotheses specialize Proposition 4.4(1),(3),(5) and Remark 4.6 to the absorbing algebra: nuclearity, simplicity, and a connected approximate half-flip in a faithful C*-completion of its algebraic tensor square. Tensor absorption follows from quotient intertwining.

lemma OAI.WeakPureInfiniteness.tensorMultiplier_polynomial_mem line 30
lemma OAI.WeakPureInfiniteness.tensorMultiplier_coefficient_dense line 47
theorem OAI.WeakPureInfiniteness.minimalTensor_equiv_of_central_embedding line 69
Source documentation
The nonunital tensor absorption argument from an actual central embedding.
```
theorem minimalTensor_equiv_of_central_embedding
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (φ : D →⋆ₐ[ℂ] NonunitalGamma.CentralSequenceAlgebra (A := A) U)
…
```
Mentions: OAI.NonunitalGamma.CentralSequenceAlgebra
theorem OAI.WeakPureInfiniteness.Campaign.nuclear_absorption_from_published_inputs line 109
Source documentation
Corollary 1.3 from the separate published central-embedding and connected-half-flip inputs, including the zero algebra. No absorption proposition is a premise.
```
theorem nuclear_absorption_from_published_inputs
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (hcentral : Nontrivial A → Nuclear A → StronglyPurelyInfinite A →
      Nonempty (OInfinity →⋆ₐ[ℂ]
        NonunitalGamma.CentralSequenceAlgebra (A := A) U))
…
```
Mentions: OAI.WeakPureInfiniteness.Nuclear, OAI.WeakPureInfiniteness.StronglyPurelyInfinite, OAI.WeakPureInfiniteness.OInfinity, OAI.NonunitalGamma.CentralSequenceAlgebra