OAI/Analysis/ModularTheory/CrossedProduct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The concrete von Neumann algebra generated by the modular coefficient representation and the regular translations. This defines the continuous core representation and its universal containment property. Semifiniteness and a trace on this algebra are not included as assumptions or assertions.

The representation is the one used in Anantharaman--Delaroche (1995), Proposition 3.6, p.329.

  1. def OAI.WeakPureInfiniteness.modularCoreGenerators line 24
  2. def OAI.WeakPureInfiniteness.algebraicModularCore line 30
  3. lemma OAI.WeakPureInfiniteness.starCentralizer_carrier line 34
  4. def OAI.WeakPureInfiniteness.modularCrossedProduct line 41
  5. lemma OAI.WeakPureInfiniteness.modularCrossedProduct_carrier line 64
  6. lemma OAI.WeakPureInfiniteness.algebraicModularCore_le line 77
  7. lemma OAI.WeakPureInfiniteness.modularCrossedProduct_coeff line 83
  8. lemma OAI.WeakPureInfiniteness.modularCrossedProduct_translate line 87
  9. def OAI.WeakPureInfiniteness.modularCoreEmbedding line 92
  10. theorem OAI.WeakPureInfiniteness.modularCoreEmbedding_injective line 97
  11. lemma OAI.WeakPureInfiniteness.modularCrossedProduct_le line 104