OAI/Algebra/Finitistic/Tensor/IdempotentTensorMaps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   An element of e'Ae acts by left multiplication on the right projectives.

   def leftMultiply (b : A) (hb : e'*b=b) : rightIdeal e →ₗ[Aᵐᵒᵖ] rightIdeal e' where
   …

   Mentions: OAI.LittleFinitistic.IdempotentTensor.rightIdeal

2. theorem OAI.LittleFinitistic.IdempotentTensor.leftMultiply_apply line 16
3. def OAI.LittleFinitistic.IdempotentTensor.splitProjection line 20

   Source documentation

   eA is a retract of the rank-one free right A-module.

   def splitProjection (he : e*e=e) : Aᵐᵒᵖ →ₗ[Aᵐᵒᵖ] rightIdeal e where
   …

   Mentions: OAI.LittleFinitistic.IdempotentTensor.rightIdeal

4. def OAI.LittleFinitistic.IdempotentTensor.splitInclusion line 25
5. theorem OAI.LittleFinitistic.IdempotentTensor.rightIdeal_projective line 30