NuclearTensorOperatorExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Extension of a nuclear commuting tensor representation to all operators in its right factor. This is the concrete extension in the commutant injectivity argument.

theorem OAI.WeakPureInfiniteness.nuclear_commuting_operator_extension line 24
Source documentation
The extension is cpc and agrees with the product on the original commuting representations. It is not asserted to be multiplicative on the larger algebra.
```
theorem nuclear_commuting_operator_extension (hA : Nuclear A)
    (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (η : C →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hη : Function.Injective η) (hc : ∀ a c, Commute (π a) (η c)) :
    letI : PartialOrder (MinimalTensor A (H →L[ℂ] H)) := CStarAlgebra.spectralOrder _
…
```
Mentions: OAI.WeakPureInfiniteness.Nuclear, OAI.WeakPureInfiniteness.MinimalTensor