CornerColumnPaths.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.CornerColumnPaths.cornerMap line 16
Source documentation
Right multiplication by the original path on the actual vertex corner.
```
def cornerMap (v i j : Fin 3) (a : ThreeVertexAlgebra μ)
    (ha : a * ThreeVertexAlgebra.vertex μ i = a) :
    CornerSpaces.corner μ v j →ₗ[k] CornerSpaces.corner μ v i where
…
```
Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.CornerSpaces.corner

theorem OAI.LittleFinitistic.CornerColumnPaths.path_naturality line 29

Source documentation

The corner-tensor identification carries the actual induced path map to right multiplication.

theorem path_naturality (v i j : Fin 3) (a : ThreeVertexAlgebra μ)
    (ha : a * ThreeVertexAlgebra.vertex μ i = a)
    (D : CochainComplex (ModuleCat.{u} (ThreeVertexAlgebra μ)ᵐᵒᵖ) ℤ) :
    TensorComplex.complexMap D (ModuleCat.ofHom (cornerMap μ v i j a ha)) ≫
        (CornerColumnComplex.complexIso μ v i D).hom =
      (CornerColumnComplex.complexIso μ v j D).hom ≫
        ((BimoduleVertex.functor k T (ThreeVertexAlgebra.vertex μ v)).mapHomologicalComplex (.up ℤ)).map
          (ExternalTensor.Section4.path k T (ThreeVertexAlgebra.vertex μ i)
            (ThreeVertexAlgebra.vertex μ j) a ha D) := by
…

Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.TensorComplex.complexMap, OAI.LittleFinitistic.CornerColumnPaths.cornerMap, OAI.LittleFinitistic.CornerColumnComplex.complexIso, OAI.LittleFinitistic.BimoduleVertex.functor, OAI.ExternalTensor.Section4.path