NuclearQuotientExpectation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The commutant projection applies to every representation of a quotient: precomposition does not change the represented algebra. This transfers the injectivity input, without assuming nuclearity of the quotient.

lemma OAI.WeakPureInfiniteness.representationCommutant_quotient line 18

theorem OAI.WeakPureInfiniteness.nuclear_quotient_commutant_expectation line 32

Source documentation

Every quotient representation has an actual cpc commutant projection.

theorem nuclear_quotient_commutant_expectation [Nontrivial H] (hA : Nuclear A)
    (q : A →⋆ₐ[ℂ] Q) (hq : Function.Surjective q) (π : Q →⋆ₐ[ℂ] (H →L[ℂ] H)) :
    ∃ P : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H), CompletelyPositive P ∧ ‖P‖ ≤ 1 ∧
      (∀ T, P T ∈ representationCommutant π) ∧
      (∀ T, T ∈ representationCommutant π → P T = T) := by
…

Mentions: OAI.WeakPureInfiniteness.Nuclear, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.WeakPureInfiniteness.representationCommutant