OAI/Algebra/Finitistic/Bimodule/BimoduleLeftTotalMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.BimoduleTotal.leftTermMap line 15

    Source documentation

    The actual tensor map induced by a bimodule-complex morphism in each bidegree.

    def leftTermMap (a q : ℤ) : Term k B P Z a q →ₗ[B] Term k B P' Z a q :=
…

    Mentions: OAI.LittleFinitistic.BimoduleTotal.Term

  2. theorem OAI.LittleFinitistic.BimoduleTotal.leftTermMap_horizontal line 18
  3. theorem OAI.LittleFinitistic.BimoduleTotal.leftTermMap_entry line 27
  4. theorem OAI.LittleFinitistic.BimoduleTotal.leftTermMap_vertical line 35
  5. def OAI.LittleFinitistic.BimoduleTotal.leftTotalMapF line 61
  6. def OAI.LittleFinitistic.BimoduleTotal.leftTotalMap line 69

    Source documentation

    Tensoring an actual bimodule chain map gives an actual B-linear total chain map.

    def leftTotalMap : total k B P p hp Z ⟶ total k B P' p hp Z where
…

    Mentions: OAI.LittleFinitistic.BimoduleTotal.total

  7. theorem OAI.LittleFinitistic.BimoduleTotal.leftTotalMap_apply line 86