VertexColumnModels.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.VertexColumnModels.cornerEquiv line 17
Source documentation
The actual vertex of an induced column is its path-corner tensor.
```
def cornerEquiv (i j : Fin 3) :
    BimoduleVertex.columnFixed μ N i j ≃ₗ[Tᵐᵒᵖ] (CornerSpaces.corner μ i j ⊗[k] N) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleVertex.columnFixed, OAI.LittleFinitistic.CornerSpaces.corner
theorem OAI.LittleFinitistic.VertexColumnModels.reverse_zero line 23
Source documentation
Vertices below the directed support have zero actual column component.
```
theorem reverse_zero (i j : Fin 3) (hij : i < j) :
    Subsingleton (BimoduleVertex.columnFixed μ N i j) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleVertex.columnFixed
theorem OAI.LittleFinitistic.VertexColumnModels.diagonal_symm_val line 38
Source documentation
The inverse diagonal equivalence is the manuscript's original insertion e_i tensor n.
```
theorem diagonal_symm_val (i : Fin 3) (n : N) :
    ((BimoduleVertex.diagonalEquiv μ N i).symm n).val =
      ExternalTensor.columnInclusion k T N (ThreeVertexAlgebra.vertex μ i) n := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleVertex.diagonalEquiv, OAI.ExternalTensor.columnInclusion, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex