OAI/RepresentationTheory/VertexAlgebra/ModuleGraphIntertwiners.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.StronglyRationalVOA.CFTTypeVOA.LocalSmear line 14
  2. abbrev OAI.StronglyRationalVOA.CFTTypeVOA.LocalGraphIndex line 21
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.LocalGraphIndex.transpose line 23
  4. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localGraphGenerator line 28
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localGraphGenerator_star line 33
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.range_localGraphGenerator line 38
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localGraphGenerator line 52
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localGraphGenerator_star line 57
  9. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.LocalGraphIntertwiner line 64
  10. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localGraphIntertwinerMap line 68
  11. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.HasTotalLocalGraphIntertwiners line 73
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.graphIntertwiners_gram_commutes line 76
  13. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localActionOfTotal line 90
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localActionOfTotal_intertwines line 95
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localActionOfTotal_normal line 101
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localActionOfTotal_generator line 106
  17. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.LocalGraphIntertwiner.restrict line 118
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.localActionOfTotal_compatible line 124
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.compatibleClosedFieldAction_of_totalGraphIntertwiners line 140