OAI/Algebra/Finitistic/Bimodule/BimoduleTotalTermMaps.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.termMap line 13
2. theorem OAI.LittleFinitistic.BimoduleTotal.termMap_comp line 26
3. theorem OAI.LittleFinitistic.BimoduleTotal.termMap_id line 40
4. def OAI.LittleFinitistic.BimoduleTotal.rightDegreeIso line 51

   Source documentation

   Right-degree transport keeps the actual balanced tensor and the full left action.

   def rightDegreeIso (P : BiComplex k B) (Z : CochainComplex (ModuleCat.{u} B) ℤ)
       (p q q' : ℤ) (h : q=q') :
       ModuleCat.of B (Term k B P Z p q) ≅ ModuleCat.of B (Term k B P Z p q') :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.Term