OAI/Algebra/Finitistic/Bimodule/BimoduleShiftHorizontal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.BimoduleTotal.termMap_transport line 14

   Source documentation

   Reindexing the unchanged input degree commutes with the original bimodule map.

   theorem termMap_transport {a b q₁ q₂ q₃ q₄ : ℤ} (f : P.X a ⟶ P.X b)
       (h₁₂ : q₁=q₂) (h₃₄ : q₃=q₄) (h₁₃ : q₁=q₃) (h₂₄ : q₂=q₄) :
       ModuleCat.ofHom (termMap (Z := Z) (Z' := Z) f (eqToHom (congrArg Z.X h₁₂))) ≫
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.termMap

2. theorem OAI.LittleFinitistic.BimoduleTotal.horizontal_shift_reindex line 25
3. theorem OAI.LittleFinitistic.BimoduleTotal.entry_shift line 36

   Source documentation

   The Koszul sign compensates exactly for the sign on the shifted horizontal differential.

   theorem entry_shift (s n m a b : ℤ) (h : n+1=m) :
       ModuleCat.ofHom (entryBetween k B P (Z⟦s⟧) n m a b h) ≫
         ((shiftColumnIso k B P Z s b).hom).f m =
       ((shiftColumnIso k B P Z s a).hom).f n ≫
         (s.negOnePow • ModuleCat.ofHom (entryBetween k B P Z (n+s) (m+s) a b (by omega))) := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.entryBetween, OAI.LittleFinitistic.BimoduleTotal.shiftColumnIso