OAI/Algebra/Finitistic/Bar/KProjectiveCoproduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.kProjectiveCoproductIsColimit line 17

   Source documentation

   An actual coproduct of K-projective cochain complexes with K-projective coproduct object remains a coproduct in the genuine derived category.

   def kProjectiveCoproductIsColimit : IsColimit (DerivedCategory.Q.mapCocone s) := by
   …