TensorArrowComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.TensorArrowComparison.component line 15
Source documentation
Tensor the actual right vertex, then identify it with the vertex of the full left B-module tensor, preserving the original balanced tensor classes.
```
def component (e : B) (he : e*e=e) (M : ModuleCat.{u} (Enveloping k B)) :
    (BalancedTensor.tensorFunctor k B N).obj ((BimoduleVertex.functor k B e).obj M) ≅
      (LeftVertexHomology.vertex k B e).obj ((BimoduleBalancedTensor.functor k B N).obj M) :=
…
```
Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.BimoduleVertex.functor, OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.BimoduleBalancedTensor.functor
theorem OAI.LittleFinitistic.TensorArrowComparison.arrow_square line 23
Source documentation
The tensor/vertex comparison retains left multiplication by every original supported arrow, and does not require the evaluation module to be flat.
```
theorem arrow_square (ei ej a : B) (hi : ei*ei=ei) (hj : ej*ej=ej) (ha : ej*a=a)
    (M : ModuleCat.{u} (Enveloping k B)) :
    (BalancedTensor.tensorFunctor k B N).map
        ((ArrowVertex.arrow k B ei ej a ha).app M) ≫ (component k B N ej hj M).hom =
      (component k B N ei hi M).hom ≫
        (LeftVertexHomology.arrow k B ei ej a ha).app ((BimoduleBalancedTensor.functor k B N).obj M) := by
…
```
Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.TensorArrowComparison.component, OAI.LittleFinitistic.LeftVertexHomology.arrow, OAI.LittleFinitistic.BimoduleBalancedTensor.functor
def OAI.LittleFinitistic.TensorArrowComparison.comparison line 45
Source documentation
Natural comparison for the full B-valued tensor functor.
```
def comparison (e : B) (he : e*e=e) :
    BimoduleVertex.functor k B e ⋙ BalancedTensor.tensorFunctor k B N ≅
      BimoduleBalancedTensor.functor k B N ⋙ LeftVertexHomology.vertex k B e :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleVertex.functor, OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.LeftVertexHomology.vertex
def OAI.LittleFinitistic.TensorArrowComparison.complexIso line 51

theorem OAI.LittleFinitistic.TensorArrowComparison.complex_arrow_square line 60

Source documentation

The full chain comparison respects the original left multiplication arrows.

theorem complex_arrow_square (ei ej a : B) (hi : ei*ei=ei) (hj : ej*ej=ej) (ha : ej*a=a)
    (P : BiComplex k B) :
    ((BalancedTensor.tensorFunctor k B N).mapHomologicalComplex (.up ℤ)).map
        (ArrowVertex.arrowComplex k B ei ej a ha P) ≫ (complexIso k B N ej hj P).hom =
      (complexIso k B N ei hi P).hom ≫
        ((LeftVertexHomology.arrow k B ei ej a ha).mapHomologicalComplex (.up ℤ)).app
          (((BimoduleBalancedTensor.functor k B N).mapHomologicalComplex (.up ℤ)).obj P) := by
…

Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.TensorArrowComparison.complexIso, OAI.LittleFinitistic.LeftVertexHomology.arrow, OAI.LittleFinitistic.BimoduleBalancedTensor.functor