OAI/Analysis/KadisonKastler/GeneratedDerivationExtension.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The concrete generated algebra and its faithful maximal quotient

This constructs the one-implementer extension used in the unital case of Sakai's argument. Its generation property is retained through the quotient. No innerness or ideal membership of the implementer is assumed here.

  1. def OAI.KadisonKastler.generatedExtensionAlgebra line 23
  2. instance OAI.KadisonKastler.generatedExtension_complete line 26
  3. instance OAI.KadisonKastler.generatedExtension_cstar line 31
  4. theorem OAI.KadisonKastler.generatedExtensionAlgebra_source line 34
  5. theorem OAI.KadisonKastler.generatedExtensionAlgebra_element line 39
  6. def OAI.KadisonKastler.generatedExtensionEmbedding line 44
  7. def OAI.KadisonKastler.generatedExtensionElement line 48
  8. theorem OAI.KadisonKastler.generatedExtension_normGenerated line 51
  9. theorem OAI.KadisonKastler.NormGeneratedExtension.map_surjective line 72
  10. theorem OAI.KadisonKastler.exists_generated_derivation_extension line 90