OAI/Analysis/BoundedHochschild/CentralAtoms.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Central atoms and their factor corners.

  1. def OAI.HochschildAtomic.center line 26
  2. instance OAI.HochschildAtomic.center_closed line 38
  3. lemma OAI.HochschildAtomic.centerClosure_eq line 46
  4. def OAI.HochschildAtomic.CenterPredual line 68
  5. instance OAI.HochschildAtomic.(instance at line 69) line 69
  6. instance OAI.HochschildAtomic.(instance at line 71) line 71
  7. instance OAI.HochschildAtomic.(instance at line 73) line 73
  8. def OAI.HochschildAtomic.centerPredualEquiv line 76
  9. theorem OAI.HochschildAtomic.scalar_center_of_projections line 85
  10. def OAI.HochschildAtomic.CentralAtom line 111
  11. lemma OAI.HochschildAtomic.corner_central_coe line 116
  12. theorem OAI.HochschildAtomic.central_atom_corner_factor line 132