OAI/Analysis/FactorGeneration/MatrixGenerators.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Diagonal projections and one full-support rank-one projection generate every finite full matrix algebra, including matrices larger than size two.

  1. def OAI.Generator.MatrixUnitSystem.fullProjectionMatrix line 18
  2. theorem OAI.Generator.MatrixUnitSystem.fullProjectionMatrix_projection line 21
  3. def OAI.Generator.MatrixUnitSystem.fullProjection line 32
  4. theorem OAI.Generator.MatrixUnitSystem.fullProjection_projection line 34
  5. theorem OAI.Generator.MatrixUnitSystem.diagonal_commute line 38
  6. theorem OAI.Generator.MatrixUnitSystem.cut_fullProjection line 44
  7. theorem OAI.Generator.MatrixUnitSystem.recover_entry line 50
  8. theorem OAI.Generator.MatrixUnitSystem.fullProjection_mem line 55
  9. theorem OAI.Generator.MatrixUnitSystem.algebra_le_of_projection_mem line 57
  10. theorem OAI.Generator.MatrixUnitSystem.algebra_eq_adjoin_projections line 64
  11. theorem OAI.Generator.countable_projection_generator line 82
  12. theorem OAI.Generator.MatrixUnitSystem.fullProjection_commute line 102
  13. theorem OAI.Generator.FiniteMatrixStage.two_generators_of_commuting_factors line 114
  14. theorem OAI.Generator.FiniteMatrixStage.concrete_le_iff line 186
  15. theorem OAI.Generator.FiniteMatrixStage.exists_commuting_factors_of_tensor_extensions line 195
  16. theorem OAI.Generator.FiniteMatrixStage.two_generators_of_tensor_extensions line 231
  17. theorem OAI.Generator.Tracial.exists_irreducible_two_generated_subfactor line 248