OAI/Algebra/Finitistic/Bimodule/BimoduleShiftCoherence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.BimoduleTotal.columnCommShift line 15
2. theorem OAI.LittleFinitistic.BimoduleTotal.column_commShiftIso_eq line 20
3. theorem OAI.LittleFinitistic.BimoduleTotal.fullColumn_map line 37
4. theorem OAI.LittleFinitistic.BimoduleTotal.functor_map_component line 48
5. theorem OAI.LittleFinitistic.BimoduleTotal.shiftTotal_hom_apply line 56
6. def OAI.LittleFinitistic.BimoduleTotal.shiftIso line 62

   Source documentation

   Naturality of the full tensor shift, in every input complex and chain map.

   def shiftIso (s : ℤ) : shiftFunctor _ s ⋙ functor k B P p hp ≅
       functor k B P p hp ⋙ shiftFunctor _ s :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.functor

7. theorem OAI.LittleFinitistic.BimoduleTotal.total_transport_apply line 84
8. theorem OAI.LittleFinitistic.BimoduleTotal.shiftIso_apply line 91
9. theorem OAI.LittleFinitistic.BimoduleTotal.shiftZero_inv_component line 96
10. theorem OAI.LittleFinitistic.BimoduleTotal.shiftAdd_inv_component line 105
11. instance OAI.LittleFinitistic.BimoduleTotal.commShift line 115

    Source documentation

    All integer shifts satisfy zero and addition coherence for the actual tensor endofunctor.

    instance commShift : (functor k B P p hp).CommShift ℤ where
    …

    Mentions: OAI.LittleFinitistic.BimoduleTotal.functor