OAI/Algebra/Finitistic/Bar/IntegerStalk.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.integerStalkIso line 13

   Source documentation

   The original nonnegative stalk maps to the actual integer derived stalk.

   def integerStalkIso (N : ModuleCat.{u} D) :
       (integerQ D).obj ((ChainComplex.single₀ (ModuleCat D)).obj N) ≅
         (DerivedCategory.singleFunctor (ModuleCat D) 0).obj N :=
   …

   Mentions: OAI.DerivedBar.integerQ