OrdinaryTensorDifferential.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.arrowMap line 16
Source documentation
The actual arrow between BC vertex projectives.
```
def arrowMap (i : Fin l) :
    IdempotentTensor.rightIdeal (TensorIdeal.vertex (k := k) (B := B) (ChainAlgebra.vertex k l i.castSucc)) →ₗ[(B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ]
…
```
Mentions: OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.vertex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra
def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.rawDifferential line 27
Source documentation
Tensor the actual arrow with O; no differential is assumed.
```
def rawDifferential (i : Fin l) : VertexTensor P a l i.castSucc →ₗ[k] VertexTensor P a l i.succ :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.VertexTensor
theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.arrow_coordinate line 30
theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.evaluation_differential line 43
Source documentation
Evaluation identifies the computed arrow differential with the genuine d_P.
```
theorem evaluation_differential (i : Fin l) (z : VertexTensor P a l i.castSucc) :
    evaluation P a l i.succ (rawDifferential P a l i z) =
      (P.d (a+(i.castSucc.val:ℤ)) (a+(i.succ.val:ℤ))).hom (evaluation P a l i.castSucc z) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.VertexTensor, OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.evaluation, OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.rawDifferential
def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.differential line 61
Source documentation
The actual tensor differential retains both B-actions.
```
def differential (i : Fin l) : VertexTensor P a l i.castSucc →ₗ[Enveloping k B] VertexTensor P a l i.succ where
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.VertexTensor, OAI.LittleFinitistic.OrdinarySimulation.Enveloping
theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.bimodule_differential_comparison line 71
Source documentation
Equality of bimodule maps, with the source's actual differential.
```
theorem bimodule_differential_comparison (i : Fin l) :
    (bimoduleEquiv P a l i.succ).toLinearMap.comp (differential P a l i) =
      (P.d (a+(i.castSucc.val:ℤ)) (a+(i.succ.val:ℤ))).hom.comp
        (bimoduleEquiv P a l i.castSucc).toLinearMap := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.bimoduleEquiv, OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.differential