OAI/Algebra/Finitistic/Bimodule/BimoduleShiftColumns.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.BimoduleTotal.fullColumn_d line 15

   Source documentation

   The B-valued column has exactly the frozen signed differential on underlying elements.

   theorem fullColumn_d (p n m : ℤ) (x : Term k B P Z p (n + -p)) :
       (((columnFunctor k B P p).obj Z).d n m).hom x =
         ((ComplexTensor.column k B (right k B P) Z p).d n m).hom x := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.BimoduleTotal.columnFunctor, OAI.LittleFinitistic.ComplexTensor.column, OAI.LittleFinitistic.BimoduleTotal.right

2. def OAI.LittleFinitistic.BimoduleTotal.shiftColumnIso line 25

   Source documentation

   The tensor shift has the Koszul sign (-1)^(s*p) on its pth column.

   def shiftColumnIso (s p : ℤ) :
       (columnFunctor k B P p).obj (Z⟦s⟧) ≅ ((columnFunctor k B P p).obj Z)⟦s⟧ :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.columnFunctor

3. def OAI.LittleFinitistic.BimoduleTotal.shiftReindex line 33
4. theorem OAI.LittleFinitistic.BimoduleTotal.shiftColumn_hom_f line 39