RelativeCentralCuntz.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative central Cuntz maps from relative local isometries

The relations are imposed after multiplication by the original algebra. Passing to the annihilator quotient gives genuine Cuntz isometries, not cpc images of such isometries.

lemma OAI.WeakPureInfiniteness.centralQuotient_eq_of_right line 32
lemma OAI.WeakPureInfiniteness.centralCuntzPair_of_relative line 41
def OAI.WeakPureInfiniteness.relativePairTest line 61
lemma OAI.WeakPureInfiniteness.relativePairTest_nonneg line 70
lemma OAI.WeakPureInfiniteness.relativePairTest_supply line 76
theorem OAI.WeakPureInfiniteness.centralOInfinityMap_of_localCuntzPair line 98
Source documentation
Local relative Cuntz relations produce an actual unital central map.
```
theorem centralOInfinityMap_of_localCuntzPair (h : LocalCentralCuntzPair A) :
    Nonempty (OInfinity →⋆ₐ[ℂ] NonunitalGamma.CentralSequenceAlgebra (A := A) U) := by
…
```
Mentions: OAI.WeakPureInfiniteness.LocalCentralCuntzPair, OAI.WeakPureInfiniteness.OInfinity, OAI.NonunitalGamma.CentralSequenceAlgebra
theorem OAI.WeakPureInfiniteness.centralOInfinityMap_of_identityDiagonalization line 162
theorem OAI.WeakPureInfiniteness.absorbsOInfinity_of_localCuntzPair line 170
Source documentation
The local multiplicative witnesses suffice for nonunital absorption once the published structural facts about OInfinity are supplied.
```
theorem absorbsOInfinity_of_localCuntzPair
    (h : LocalCentralCuntzPair A)
    (hD : Pureness.IsNuclear.{1,1} OInfinity)
    (hs : Pureness.TopologicallySimple OInfinity)
    {T : Type*} [CStarAlgebra T]
    (f : OInfinity ⊗[ℂ] OInfinity →⋆ₐ[ℂ] T)
    (hf : Function.Injective f) (hd : DenseRange f)
    (hh : CStarAbsorption.ConnectedApproximateInnerHalfFlip f) :
    AbsorbsOInfinity A := by
…
```
Mentions: OAI.WeakPureInfiniteness.LocalCentralCuntzPair, OAI.WeakPureInfiniteness.OInfinity, OAI.Pureness.TopologicallySimple, OAI.CStarAbsorption.ConnectedApproximateInnerHalfFlip, OAI.WeakPureInfiniteness.AbsorbsOInfinity