OAI/Algebra/Finitistic/Tensor/BalancedVertexImage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BalancedVertexImage.V line 19
2. abbrev OAI.LittleFinitistic.BalancedVertexImage.W line 20
3. abbrev OAI.LittleFinitistic.BalancedVertexImage.F line 21
4. def OAI.LittleFinitistic.BalancedVertexImage.inclusion line 23
5. def OAI.LittleFinitistic.BalancedVertexImage.projection line 26
6. theorem OAI.LittleFinitistic.BalancedVertexImage.split line 30
7. theorem OAI.LittleFinitistic.BalancedVertexImage.projector line 35
8. def OAI.LittleFinitistic.BalancedVertexImage.fixedEquiv line 42

   Source documentation

   The image of the original vertex projector after tensoring is the actual left vertex.

   def fixedEquiv :
       AdditiveSplitImage.fixed (F k B N) (inclusion k B M e) (projection k B M e he) ≃ₗ[k]
         IdempotentTensor.leftSpace (k := k) e (BimoduleBalancedTensor.Tensor k B M N) where
   …

   Mentions: OAI.LittleFinitistic.AdditiveSplitImage.fixed, OAI.LittleFinitistic.BalancedVertexImage.F, OAI.LittleFinitistic.BalancedVertexImage.inclusion, OAI.LittleFinitistic.BalancedVertexImage.projection, OAI.LittleFinitistic.IdempotentTensor.leftSpace, OAI.LittleFinitistic.BimoduleBalancedTensor.Tensor

9. def OAI.LittleFinitistic.BalancedVertexImage.equiv line 59

   Source documentation

   Vertex extraction commutes with actual balanced tensoring, without a flatness assumption.

   def equiv : (F k B N).obj (V k B M e) ≃ₗ[k]
       IdempotentTensor.leftSpace (k := k) e (BimoduleBalancedTensor.Tensor k B M N) :=
   …

   Mentions: OAI.LittleFinitistic.BalancedVertexImage.F, OAI.LittleFinitistic.BalancedVertexImage.V, OAI.LittleFinitistic.IdempotentTensor.leftSpace, OAI.LittleFinitistic.BimoduleBalancedTensor.Tensor

10. theorem OAI.LittleFinitistic.BalancedVertexImage.equiv_apply_val line 64