OAI/Analysis/Nuclearity/UnitizedTensorElementary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Elementary tensors in the original nonunital tensor ideal have their first factor in the original algebra. This is the elementary lifting step in transferring ideal generation from a unitization.

  1. def OAI.WeakPureInfiniteness.unitizationScalarHom line 16
  2. def OAI.WeakPureInfiniteness.unitizedTensorInclusion line 24
  3. def OAI.WeakPureInfiniteness.unitizedTensorScalar line 27
  4. theorem OAI.WeakPureInfiniteness.unitizedTensorInclusion_isometry line 30
  5. theorem OAI.WeakPureInfiniteness.unitizedTensorInclusion_elementary line 33
  6. theorem OAI.WeakPureInfiniteness.unitizedTensorScalar_elementary line 37
  7. theorem OAI.WeakPureInfiniteness.unitizedTensorScalar_inclusion line 41
  8. theorem OAI.WeakPureInfiniteness.unitizedTensor_elementary_lift line 51