OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorVertex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.tensor_smul line 14
2. theorem OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.tensor_vertex_smul line 17
3. def OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.tensorVertexSpaceEquiv line 24

   Source documentation

   The BC vertex space is the same actual subspace of O as the C vertex space.

   def tensorVertexSpaceEquiv (i : Fin (l+1)) :
       IdempotentTensor.leftSpace (k := k) (TensorIdeal.vertex (k := k) (B := B) (ChainAlgebra.vertex k l i))
   …

   Mentions: OAI.LittleFinitistic.IdempotentTensor.leftSpace, OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.vertex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex

4. def OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.tensorVertexEquiv line 40

   Source documentation

   Evaluation uses the actual balanced tensor over BC, not only over C.

   def tensorVertexEquiv (i : Fin (l+1)) :
       BalancedTensor.Tensor k (B ⊗[k] ChainAlgebra k l)
         (IdempotentTensor.rightIdeal (TensorIdeal.vertex (k := k) (B := B) (ChainAlgebra.vertex k l i)))
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.vertex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex