OAI/Algebra/Finitistic/Bimodule/BimoduleTotalShortExact.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.leftTotalFunctor line 16

   Source documentation

   Fixed-input finite tensor total as an actual functor on bimodule complexes.

   def leftTotalFunctor : BiComplex k B ⥤ CochainComplex (ModuleCat.{u} B) ℤ where
   …

2. instance OAI.LittleFinitistic.BimoduleTotal.leftTotalFunctor_preservesZeroMorphisms line 22
3. theorem OAI.LittleFinitistic.BimoduleTotal.leftTotal_shortExact line 36

   Source documentation

   Short exact sequences of bimodules remain short exact after the finite total on an input complex of projective left modules.

   theorem leftTotal_shortExact (S : ShortComplex (BiComplex k B)) (hS : S.ShortExact) :
       (S.map (leftTotalFunctor k B Z p hp)).ShortExact := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.leftTotalFunctor