OAI/Algebra/Finitistic/Ordinary/OrdinaryChainAlgebra.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra line 16

    Source documentation

    The radical-square-zero chain algebra, in vertex and arrow coordinates. Arrow i goes from i to i+1, with the manuscript's right-projective convention.

    def ChainAlgebra := (Fin (l+1) → k) × (Fin l → k)
…
  2. instance OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.(instance at line 18) line 18
  3. instance OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.(instance at line 20) line 20
  4. instance OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.(instance at line 22) line 22
  5. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.zero_eq line 25
  6. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.add_eq line 26
  7. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.smul_eq line 27
  8. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.diagonal line 29
  9. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.radical line 30
  10. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.mul line 32
  11. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.unit line 35
  12. instance OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.(instance at line 37) line 37
  13. instance OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.(instance at line 65) line 65
  14. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.mul_diagonal line 89
  15. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.mul_radical line 91
  16. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex line 94
  17. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow line 95
  18. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex_idempotent line 97
  19. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow_mul_arrow line 105
  20. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex_target_arrow line 110
  21. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow_vertex_source line 118
  22. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalCharacter line 127

    Source documentation

    The terminal simple right module is the character at vertex l.

    def terminalCharacter : ChainAlgebra k l →ₐ[k] k where
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

  23. abbrev OAI.LittleFinitistic.OrdinarySimulation.AlgebraD line 138

    Source documentation

    The actual ordinary algebra D of Section 5.

    abbrev AlgebraD := B × (B ⊗[k] ChainAlgebra k l)

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

  24. instance OAI.LittleFinitistic.OrdinarySimulation.finiteDimensionalD line 139