OAI/Analysis/Nuclearity/RepresentedTensorKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The factor-image kernel formula in Tomiyama's Theorem 5. Nuclearity of the actual represented left quotient remains an explicit input.

  1. abbrev OAI.WeakPureInfiniteness.UnitalTensorRepresentation line 22
  2. def OAI.WeakPureInfiniteness.unitalTensorRepresentationNonunital line 26
  3. def OAI.WeakPureInfiniteness.representedTensorQuotient line 36
  4. theorem OAI.WeakPureInfiniteness.representedTensorQuotient_elementary line 39
  5. theorem OAI.WeakPureInfiniteness.representedTensorQuotient_kernel line 44