OAI/Algebra/Finitistic/Ordinary/OrdinaryBimodule.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.OrdinarySimulation.Enveloping line 11
  2. def OAI.LittleFinitistic.OrdinarySimulation.BimoduleO line 14

    Source documentation

    O from the genuine dg B-bimodule, as an ordinary finite sum of its terms.

    def BimoduleO (P : CochainComplex (ModuleCat.{u} (Enveloping k B)) ℤ)
    (a : ℤ) (l : ℕ) := Compression P a l
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.Enveloping, OAI.LittleFinitistic.OrdinarySimulation.Compression

  3. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 19) line 19
  4. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 20) line 20
  5. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 21) line 21
  6. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 22) line 22
  7. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 23) line 23
  8. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 25) line 25
  9. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 27) line 27
  10. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 29) line 29
  11. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.(instance at line 32) line 32
  12. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.towerLeft line 35
  13. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.towerRight line 43
  14. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.commuteLeftRight line 51
  15. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.commuteChainLeft line 59
  16. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.commuteChainRight line 65
  17. def OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.leftAction line 72

    Source documentation

    The left B tensor C action takes values in actual right-B-linear maps.

    def leftAction : (B ⊗[k] ChainAlgebra k l) →ₐ[k] Module.End Bᵐᵒᵖ (BimoduleO P a l) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.BimoduleO

  18. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.leftModule line 79
  19. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.towerTensor line 82
  20. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.commuteTensorRight line 88
  21. instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.finiteDimensional line 91