OAI/Algebra/Finitistic/Ordinary/OrdinaryFirstDerivedRetraction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BlockModule.derivedFirstComponent line 14

   Source documentation

   The exact derived first-component functor on the whole product-ring derived category.

   abbrev derivedFirstComponent := (ProductModules.firstFunctor.{u,u} L R).mapDerivedCategory

2. def OAI.LittleFinitistic.BlockModule.firstComplexComponentIso line 16
3. def OAI.LittleFinitistic.BlockModule.derivedFirstComponentFactors line 23

   Source documentation

   On chain representatives, the composite is the identity localization.

   def derivedFirstComponentFactors : DerivedCategory.Q ⋙ derivedFirst L R ⋙
       derivedFirstComponent L R ≅ (DerivedCategory.Q : CochainComplex (ModuleCat.{u} L) ℤ ⥤ _) :=
   …

   Mentions: OAI.LittleFinitistic.BlockModule.derivedFirst, OAI.LittleFinitistic.BlockModule.derivedFirstComponent

4. def OAI.LittleFinitistic.BlockModule.derivedFirstRetraction line 33

   Source documentation

   Taking the first component recovers every derived object, naturally.

   def derivedFirstRetraction : derivedFirst L R ⋙ derivedFirstComponent L R ≅
       𝟭 (DerivedCategory (ModuleCat.{u} L)) := by
   …

   Mentions: OAI.LittleFinitistic.BlockModule.derivedFirst, OAI.LittleFinitistic.BlockModule.derivedFirstComponent

5. def OAI.LittleFinitistic.BlockModule.exactFirstRetraction line 43

   Source documentation

   The same retraction for mathlib's exact derived inflation.

   def exactFirstRetraction : (ProductModules.firstInflation L R).mapDerivedCategory ⋙
       derivedFirstComponent L R ≅ 𝟭 (DerivedCategory (ModuleCat.{u} L)) :=
   …

   Mentions: OAI.LittleFinitistic.ProductModules.firstInflation, OAI.LittleFinitistic.BlockModule.derivedFirstComponent

6. instance OAI.LittleFinitistic.BlockModule.derivedFirst_additive line 47
7. theorem OAI.LittleFinitistic.BlockModule.derivedFirst_isZero_iff line 51

   Source documentation

   No derived object becomes zero merely by putting it in the first block.

   theorem derivedFirst_isZero_iff (Y : DerivedCategory (ModuleCat.{u} L)) :
       IsZero ((derivedFirst L R).obj Y) ↔ IsZero Y := by
   …

   Mentions: OAI.LittleFinitistic.BlockModule.derivedFirst

8. theorem OAI.LittleFinitistic.BlockModule.exactFirst_isZero_iff line 59