OAI/Algebra/Finitistic/Tensor/BalancedVertexFunctor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BalancedVertexFunctor.Space line 14
2. def OAI.LittleFinitistic.BalancedVertexFunctor.spaceMap line 17
3. def OAI.LittleFinitistic.BalancedVertexFunctor.functor line 27

   Source documentation

   The actual left vertex of the balanced tensor, with its original induced maps.

   def functor : ModuleCat.{u} (Enveloping k B) ⥤ ModuleCat.{u} k where
   …

4. instance OAI.LittleFinitistic.BalancedVertexFunctor.additive line 46
5. def OAI.LittleFinitistic.BalancedVertexFunctor.comparison line 58

   Source documentation

   Vertex extraction commutes naturally with the original balanced tensor functor.

   def comparison : BimoduleVertex.functor k B e ⋙ BalancedTensor.tensorFunctor k B N ≅
       functor k B e N :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleVertex.functor, OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.BalancedVertexFunctor.functor

6. def OAI.LittleFinitistic.BalancedVertexFunctor.complexIso line 77

   Source documentation

   The natural comparison gives an actual chain isomorphism on every bimodule complex.

   def complexIso (P : BiComplex k B) :
       ((BimoduleVertex.functor k B e ⋙ BalancedTensor.tensorFunctor k B N).mapHomologicalComplex (.up ℤ)).obj P ≅
         ((functor k B e N).mapHomologicalComplex (.up ℤ)).obj P :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleVertex.functor, OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.BalancedVertexFunctor.functor