OAI/Analysis/BoundedHochschild/CentralComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Comparison of projections using central weighted traces.

  1. lemma OAI.HochschildCentralComparison.orthogonal_of_le_sub line 26
  2. lemma OAI.HochschildCentralComparison.exists_maximal_partialIso line 37
  3. theorem OAI.HochschildCentralComparison.central_comparison line 77
  4. lemma OAI.HochschildCentralComparison.central_weighted_trace_partialIso line 97
  5. theorem OAI.HochschildCentralComparison.subequivalent_of_central_trace_le line 107
  6. theorem OAI.HochschildCentralComparison.equivalent_of_central_trace_eq line 142