OAI/Algebra/Finitistic/Ordinary/OrdinaryBlockDerived.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BlockModule.firstComplexFunctor line 14
2. theorem OAI.LittleFinitistic.BlockModule.first_inverts line 17
3. def OAI.LittleFinitistic.BlockModule.derivedFirst line 26

   Source documentation

   Native derived inflation on the first block of the product algebra.

   def derivedFirst : DerivedCategory (ModuleCat.{u} L) ⥤ DerivedCategory (ModuleCat.{u} (L × R)) :=
   …

4. def OAI.LittleFinitistic.BlockModule.derivedFirstComparison line 29