OAI/Algebra/Finitistic/Tensor/BalancedTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BalancedTensor.relations line 15

   Source documentation

   Balancing relations for a right A-module and a left A-module, over k.

   def relations : Submodule k (M ⊗[k] N) := Submodule.span k
   …

2. abbrev OAI.LittleFinitistic.BalancedTensor.Tensor line 20

   Source documentation

   Tensor over the possibly noncommutative algebra A.

   abbrev Tensor := (M ⊗[k] N) ⧸ relations k A M N

   Mentions: OAI.LittleFinitistic.BalancedTensor.relations

3. def OAI.LittleFinitistic.BalancedTensor.mk line 22
4. theorem OAI.LittleFinitistic.BalancedTensor.balance line 27
5. def OAI.LittleFinitistic.BalancedTensor.lift line 39

   Source documentation

   Universal property for k-bilinear maps satisfying the actual A-balancing equation.

   def lift (f : M →ₗ[k] N →ₗ[k] V)
       (hf : ∀ (a : A) m n, f (MulOpposite.op a • m) n = f m (a • n)) : Tensor k A M N →ₗ[k] V :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

6. theorem OAI.LittleFinitistic.BalancedTensor.lift_mk line 47
7. theorem OAI.LittleFinitistic.BalancedTensor.induction_on line 51
8. theorem OAI.LittleFinitistic.BalancedTensor.ext line 64