OAI/Algebra/Finitistic/Ordinary/OrdinaryBlockBimodule.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal line 11

    Source documentation

    The off-diagonal ordinary bimodule O ⊕ T over L × R.

    def OffDiagonal (O T : Type u) := O × T
…
  2. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.(instance at line 13) line 13
  3. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.(instance at line 14) line 14
  4. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.leftModule line 17
  5. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.rightModule line 22
  6. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.commuteActions line 28
  7. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.towerLeft line 38
  8. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.towerRight line 43
  9. instance OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.finiteDimensional line 49
  10. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.first_left line 54

    Source documentation

    The first left block selects precisely T.

    theorem first_left [Module R O] [Module L T] (x : OffDiagonal O T) :
    ((1,0) : L × R) • x = (0,x.2) := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal

  11. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.first_right line 61

    Source documentation

    The first right block selects precisely O.

    theorem first_right [Module Lᵐᵒᵖ O] [Module Rᵐᵒᵖ T] (x : OffDiagonal O T) :
    MulOpposite.op ((1,0) : L × R) • x = (x.1,0) := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal

  12. abbrev OAI.LittleFinitistic.OrdinarySimulation.BimoduleX line 73

    Source documentation

    The actual ordinary Section 5 bimodule X over D=B×(B tensor C).

    abbrev BimoduleX (P : CochainComplex (ModuleCat.{u} (Enveloping k B)) ℤ) (a : ℤ) (l : ℕ) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.Enveloping

  13. theorem OAI.LittleFinitistic.OrdinarySimulation.ordinary_bimodule line 76
  14. theorem OAI.LittleFinitistic.OrdinarySimulation.ordinary_finite line 80