BimoduleTensorVertexBridge.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleTensorVertexBridge.equiv line 17
Source documentation
The full B-valued tensor functor has exactly the previously constructed vertex spaces, with scalar restriction accounted for explicitly.
```
def equiv (e : B) (M : ModuleCat.{u} (Enveloping k B)) :
    (LeftVertexHomology.vertex k B e).obj ((BimoduleBalancedTensor.functor k B N).obj M) ≃ₗ[k]
      BalancedVertexFunctor.Space k B e N M where
…
```
Mentions: OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BalancedVertexFunctor.Space
def OAI.LittleFinitistic.BimoduleTensorVertexBridge.comparison line 30
Source documentation
All induced differential and module maps are retained by the comparison.
```
def comparison (e : B) : BimoduleBalancedTensor.functor k B N ⋙
    LeftVertexHomology.vertex k B e ≅ BalancedVertexFunctor.functor k B e N :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.BalancedVertexFunctor.functor
def OAI.LittleFinitistic.BimoduleTensorVertexBridge.complexIso line 41
Source documentation
An actual chain comparison with the vertex of the full B-module tensor complex.
```
def complexIso (e : B) (P : BiComplex k B) :
    (((LeftVertexHomology.vertex k B e).mapHomologicalComplex (.up ℤ)).obj
      (((BimoduleBalancedTensor.functor k B N).mapHomologicalComplex (.up ℤ)).obj P)) ≅
      (((BalancedVertexFunctor.functor k B e N).mapHomologicalComplex (.up ℤ)).obj P) :=
…
```
Mentions: OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BalancedVertexFunctor.functor