OAI/Analysis/Nuclearity/MatrixCPMapExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Extension of a cpc map with finite matrix codomain along an injective unital star homomorphism. The proof extends the associated positive scalar functional and reconstructs the matrix map from its GNS representation.

  1. lemma OAI.WeakPureInfiniteness.cp_norm_le_one_of_one line 19
  2. def OAI.WeakPureInfiniteness.matrixUnitalMap line 39
  3. lemma OAI.WeakPureInfiniteness.matrixUnitalMap_injective line 55
  4. lemma OAI.WeakPureInfiniteness.cpMatrixFunctional_single line 62
  5. lemma OAI.WeakPureInfiniteness.matrixUnitalMap_single line 86
  6. theorem OAI.WeakPureInfiniteness.matrix_cpc_extension line 92