OAI/Algebra/Finitistic/Bimodule/BimoduleBarIteration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.nativeIterate line 17

   Source documentation

   Iteration of the native full-left-action integer derived endofunctor.

   def nativeIterate : ℕ → (DerivedCategory (ModuleCat.{u} B) ⥤ DerivedCategory (ModuleCat.{u} B))
     | 0 => 𝟭 _
     | r+1 => nativeIterate r ⋙ res.data.derived
   
   /-- The augmentation comparison iterates naturally on the genuine localized
   chain category. This identifies actual derived functors, not only vector spaces. -/

   Mentions: OAI.LittleFinitistic.BimoduleTotal.derived

2. def OAI.LittleFinitistic.BimoduleTotal.nativeBarIterateIso line 23

   Source documentation

   The augmentation comparison iterates naturally on the genuine localized chain category. This identifies actual derived functors, not only vector spaces.

   def nativeBarIterateIso : (r : ℕ) →
       DerivedBar.chainToIntegerDerived B ⋙ nativeIterate res r ≅
         DerivedBar.derivedTensorIterate k B (barModule (X := X)) r ⋙ DerivedBar.chainToIntegerDerived B
   …

   Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.LittleFinitistic.BimoduleTotal.nativeIterate, OAI.DerivedBar.derivedTensorIterate, OAI.LittleFinitistic.BimoduleTotal.barModule

3. def OAI.LittleFinitistic.BimoduleTotal.nativeIterateMultibarIso line 37

   Source documentation

   The native iterate on an extended chain input is the manuscript's actual recursive bar total, with the endpoint-minus-tail and signed vertical differentials.

   def nativeIterateMultibarIso (Z : ChainComplex (ModuleCat.{u} B) ℕ) (r : ℕ) :
       (nativeIterate res r).obj ((DerivedBar.integerQ B).obj Z) ≅
         (DerivedBar.integerQ B).obj (DerivedBar.explicitMultibar k B (barModule (X := X)) r Z) :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.nativeIterate, OAI.DerivedBar.integerQ, OAI.DerivedBar.explicitMultibar, OAI.LittleFinitistic.BimoduleTotal.barModule

4. def OAI.LittleFinitistic.BimoduleTotal.nativeIterateIndexedIso line 48

   Source documentation

   On degree-zero modules, the same native derived iteration is represented by the actual Section 6 indexed multibar with all module actions retained.

   def nativeIterateIndexedIso (N : ModuleCat.{u} B) (r : ℕ) :
       (nativeIterate res r).obj ((DerivedBar.integerQ B).obj ((ChainComplex.single₀ _).obj N)) ≅
         DerivedCategory.Q.obj ((DerivedBar.integerExtension B).obj
           (DerivedBar.RecursiveTotal.indexedMultibar k B (barModule (X := X)) N r)) :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.nativeIterate, OAI.DerivedBar.integerQ, OAI.DerivedBar.integerExtension, OAI.DerivedBar.RecursiveTotal.indexedMultibar, OAI.LittleFinitistic.BimoduleTotal.barModule