OAI/Algebra/Finitistic/Ordinary/OrdinaryBalancedActions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BalancedTensor.mapRight line 14

   Source documentation

   Tensor an actual left-module homomorphism with the identity.

   def mapRight (f : N →ₗ[A] N) : Tensor k A M N →ₗ[k] Tensor k A M N :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

2. theorem OAI.LittleFinitistic.BalancedTensor.mapRight_mk line 21
3. def OAI.LittleFinitistic.BalancedTensor.leftAction line 28

   Source documentation

   The left coefficient action is induced from the first balanced-tensor factor.

   def leftAction : S →ₐ[k] Module.End k (Tensor k A M N) where
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

4. theorem OAI.LittleFinitistic.BalancedTensor.leftAction_mk line 37
5. def OAI.LittleFinitistic.BalancedTensor.rightAction line 44

   Source documentation

   The right coefficient action is induced from the second balanced-tensor factor.

   def rightAction : T →ₐ[k] Module.End k (Tensor k A M N) where
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

6. theorem OAI.LittleFinitistic.BalancedTensor.rightAction_mk line 53
7. def OAI.LittleFinitistic.BalancedTensor.bimoduleAction line 57

   Source documentation

   Both outside actions on a balanced tensor, combined without forgetting either factor.

   def bimoduleAction : (S ⊗[k] T) →ₐ[k] Module.End k (Tensor k A M N) :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

8. theorem OAI.LittleFinitistic.BalancedTensor.bimoduleAction_tmul_mk line 65