AbsorptionFromCentralCopy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absorption from a central embedding and a connected approximate half-flip, using the nuclearity and simplicity of O∞ and Kirchberg's criterion.

theorem OAI.WeakPureInfiniteness.Campaign.nuclear_absorption_from_central_embedding_and_halfFlip line 25
Source documentation
The full absorption corollary, still conditional on the published central embedding and connected half-flip; O∞ nuclearity and simplicity are proved.
```
theorem nuclear_absorption_from_central_embedding_and_halfFlip
    (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