CornerColumnComplex.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.CornerColumnComplex.cornerToIdeal line 17
Source documentation
Embed an actual corner into the principal left ideal of its source vertex.
```
def cornerToIdeal (i j : Fin 3) : CornerSpaces.corner μ i j →ₗ[k]
    ExternalTensor.leftIdeal T (ThreeVertexAlgebra.vertex μ j) where
…
```
Mentions: OAI.LittleFinitistic.CornerSpaces.corner, OAI.ExternalTensor.leftIdeal, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex
theorem OAI.LittleFinitistic.CornerColumnComplex.corner_symm_tmul_val line 24
Source documentation
The corner equivalence retains the actual tensor insertion on pure tensors.
```
theorem corner_symm_tmul_val (N : ModuleCat.{u} (ThreeVertexAlgebra μ)ᵐᵒᵖ)
    (i j : Fin 3) (x : CornerSpaces.corner μ i j) (n : N) :
    ((VertexColumnModels.cornerEquiv μ N i j).symm (x ⊗ₜ[k] n)).val =
      cornerToIdeal μ i j x ⊗ₜ[k] n := by
…
```
Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.CornerSpaces.corner, OAI.LittleFinitistic.VertexColumnModels.cornerEquiv, OAI.LittleFinitistic.CornerColumnComplex.cornerToIdeal
def OAI.LittleFinitistic.CornerColumnComplex.complexIso line 31
Source documentation
Every actual vertex column is its concrete corner-tensor complex.
```
def complexIso (i j : Fin 3)
    (D : CochainComplex (ModuleCat.{u} (ThreeVertexAlgebra μ)ᵐᵒᵖ) ℤ) :
    TensorComplex.complex D (ModuleCat.of k (CornerSpaces.corner μ i j)) ≅
      ((VertexColumnComplex.vertexColumn μ i j).mapHomologicalComplex (.up ℤ)).obj D :=
…
```
Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.TensorComplex.complex, OAI.LittleFinitistic.CornerSpaces.corner, OAI.LittleFinitistic.VertexColumnComplex.vertexColumn