OAI/Algebra/Finitistic/Bar/TotalBarFunctor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.barTotalFunctor line 15

   Source documentation

   The total bar resolution is a functor on nonnegative chain complexes.

   def barTotalFunctor : ChainComplex (ModuleCat.{u} A) ℕ ⥤ ChainComplex (ModuleCat.{u} A) ℕ :=
   …

2. theorem OAI.DerivedBar.ι_barTotalFunctor_map line 20
3. theorem OAI.DerivedBar.augmentation_zero_diagonal line 29
4. def OAI.DerivedBar.barTotalAugmentationNat line 37

   Source documentation

   The augmentation is natural for all chain maps, not only quasi-isomorphisms.

   def barTotalAugmentationNat : barTotalFunctor k A ⟶ 𝟭 _ where
   …

   Mentions: OAI.DerivedBar.barTotalFunctor