CornerTensor.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.CornerTensor.cornerTensorEquiv line 20
Source documentation
The concrete corner tensor is the fixed submodule of the induced column.
```
def cornerTensorEquiv (i j : Fin 3) :
    (corner μ i j ⊗[k] N) ≃ₗ[(ThreeVertexAlgebra μ)ᵐᵒᵖ]
    TensorProjection.fixed (B := ThreeVertexAlgebra μ) (N := N) (projection μ i j) :=
…
```
Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.TensorProjection.fixed
theorem OAI.LittleFinitistic.CornerTensor.fixed_iff_left_action line 28
Source documentation
This fixed-space definition uses the original left vertex action on the column.
```
theorem fixed_iff_left_action (i j : Fin 3)
    (x : ExternalTensor.Column k (ThreeVertexAlgebra μ) N (vertex μ j)) :
    x ∈ TensorProjection.fixed (B := ThreeVertexAlgebra μ) (projection μ i j) ↔
…
```
Mentions: OAI.ExternalTensor.Column, OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.TensorProjection.fixed
def OAI.LittleFinitistic.CornerTensor.scalarTensorEquiv line 40
Source documentation
Scalar tensor multiplication is right B-linear with the actual external action.
```
def scalarTensorEquiv : (k ⊗[k] N) ≃ₗ[(ThreeVertexAlgebra μ)ᵐᵒᵖ] N where
…
```
Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra
def OAI.LittleFinitistic.CornerTensor.diagonalColumnEquiv line 50
Source documentation
The diagonal vertex component of its own induced column is exactly N.
```
def diagonalColumnEquiv (i : Fin 3) :
    TensorProjection.fixed (B := ThreeVertexAlgebra μ) (N := N) (projection μ i i)
…
```
Mentions: OAI.LittleFinitistic.TensorProjection.fixed, OAI.LittleFinitistic.ThreeVertexAlgebra