MultiplierIntertwining.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Restricting multiplier conjugacies to a nonunital algebra

The range of the canonical map into the multiplier algebra is an ideal. Consequently tensor conjugacies constructed in the multiplier algebra restrict to the original, possibly nonunital, tensor product. This is the local nonunital step in the central-embedding absorption argument; no central embedding or absorption statement is assumed here.

def OAI.WeakPureInfiniteness.RightIdealRange line 31
Source documentation
A formulation of right-ideal range useful for nonunital embeddings.
```
def RightIdealRange (ι : A →⋆ₙₐ[ℂ] B) : Prop :=
…
```
lemma OAI.WeakPureInfiniteness.RightIdealRange.mul_left line 34
lemma OAI.WeakPureInfiniteness.RightIdealRange.inner_mem line 39
def OAI.WeakPureInfiniteness.RightIdealRange.restrictInner line 56
Source documentation
Restrict an inner automorphism of the containing algebra to its ideal.
```
def RightIdealRange.restrictInner {ι : A →⋆ₙₐ[ℂ] B} (h : RightIdealRange ι)
    (hι : Function.Injective ι) (u : unitary (Unitization ℂ B)) : A ≃⋆ₐ[ℂ] A := by
…
```
Mentions: OAI.WeakPureInfiniteness.RightIdealRange
lemma OAI.WeakPureInfiniteness.RightIdealRange.restrictInner_apply line 75
lemma OAI.WeakPureInfiniteness.multiplierInclusion_injective line 89
lemma OAI.WeakPureInfiniteness.multiplierInclusion_rightIdeal line 96
lemma OAI.WeakPureInfiniteness.minimalMapLeft_isometry_any line 121
lemma OAI.WeakPureInfiniteness.RightIdealRange.tensor line 132