OAI/Algebra/Finitistic/Tensor/IdempotentTensor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.IdempotentTensor.rightIdeal line 11

   Source documentation

   The actual projective right ideal eA, presented as the fixed points of left multiplication.

   def rightIdeal : Submodule Aᵐᵒᵖ A where
   …

2. def OAI.LittleFinitistic.IdempotentTensor.leftSpace line 23

   Source documentation

   The vertex part eN, without assuming e is central.

   def leftSpace : Submodule k N where
   …

3. def OAI.LittleFinitistic.IdempotentTensor.productEval line 29
4. def OAI.LittleFinitistic.IdempotentTensor.tensorEval line 38

   Source documentation

   The natural map eA tensor_A N → eN.

   def tensorEval : BalancedTensor.Tensor k A (rightIdeal e) N →ₗ[k] leftSpace (k := k) e N :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.IdempotentTensor.leftSpace

5. theorem OAI.LittleFinitistic.IdempotentTensor.tensorEval_mk line 44
6. def OAI.LittleFinitistic.IdempotentTensor.tensorInv line 49
7. theorem OAI.LittleFinitistic.IdempotentTensor.tensorEval_tensorInv line 52
8. theorem OAI.LittleFinitistic.IdempotentTensor.tensorInv_tensorEval line 57
9. def OAI.LittleFinitistic.IdempotentTensor.tensorEquiv line 72

   Source documentation

   Evaluation on a vertex projective is its actual vertex space.

   def tensorEquiv : BalancedTensor.Tensor k A (rightIdeal e) N ≃ₗ[k] leftSpace (k := k) e N where
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.IdempotentTensor.leftSpace