OAI/Algebra/Finitistic/Ordinary/OrdinaryTwoSidedTensor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.TwoSidedTensor line 9

   Source documentation

   Balanced tensor with its two outside coefficient algebras recorded in the type.

   def TwoSidedTensor (k A _S _T M N : Type u) [Field k] [Ring A] [Algebra k A]
       [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M]
       [AddCommGroup N] [Module k N] [Module A N] := BalancedTensor.Tensor k A M N
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

2. instance OAI.LittleFinitistic.TwoSidedTensor.(instance at line 21) line 21
3. instance OAI.LittleFinitistic.TwoSidedTensor.(instance at line 22) line 22
4. def OAI.LittleFinitistic.TwoSidedTensor.action line 24
5. instance OAI.LittleFinitistic.TwoSidedTensor.(instance at line 26) line 26
6. instance OAI.LittleFinitistic.TwoSidedTensor.(instance at line 27) line 27
7. def OAI.LittleFinitistic.TwoSidedTensor.mk line 33
8. theorem OAI.LittleFinitistic.TwoSidedTensor.tmul_smul_mk line 35
9. def OAI.LittleFinitistic.TwoSidedTensor.map line 43

   Source documentation

   Functoriality of the actual tensor with both outside actions retained.

   def map (f : M →ₗ[Aᵐᵒᵖ] M') (hf : ∀ (s : S) m, f (s • m) = s • f m) :
       TwoSidedTensor k A S T M N →ₗ[S ⊗[k] T] TwoSidedTensor k A S T M' N where
   …

   Mentions: OAI.LittleFinitistic.TwoSidedTensor

10. theorem OAI.LittleFinitistic.TwoSidedTensor.map_mk line 61
11. def OAI.LittleFinitistic.TwoSidedTensor.congrLeft line 65

    Source documentation

    Actual equivalences of the right factor on the left preserve the outside bimodule.

    def congrLeft (e : M ≃ₗ[Aᵐᵒᵖ] M') (he : ∀ (s : S) m, e (s • m) = s • e m) :
        TwoSidedTensor k A S T M N ≃ₗ[S ⊗[k] T] TwoSidedTensor k A S T M' N where
    …

    Mentions: OAI.LittleFinitistic.TwoSidedTensor