OAI/Algebra/Finitistic/Tensor/BalancedFreeLeft.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BalancedTensor.FreeLeft.coefficientAction line 12

   Source documentation

   A coefficient of a free left module acts on the right tensor factor.

   def coefficientAction : A →ₗ[k] M →ₗ[k] M :=
   …

2. def OAI.LittleFinitistic.BalancedTensor.FreeLeft.evaluateBilinear line 15
3. theorem OAI.LittleFinitistic.BalancedTensor.FreeLeft.evaluateBilinear_single line 19
4. def OAI.LittleFinitistic.BalancedTensor.FreeLeft.evaluation line 25
5. theorem OAI.LittleFinitistic.BalancedTensor.FreeLeft.evaluation_single line 37
6. def OAI.LittleFinitistic.BalancedTensor.FreeLeft.insertion line 41
7. theorem OAI.LittleFinitistic.BalancedTensor.FreeLeft.insertion_single line 45
8. theorem OAI.LittleFinitistic.BalancedTensor.FreeLeft.evaluation_insertion line 50
9. theorem OAI.LittleFinitistic.BalancedTensor.FreeLeft.insertion_evaluation line 57
10. def OAI.LittleFinitistic.BalancedTensor.FreeLeft.equivalence line 72

    Source documentation

    Tensor with an arbitrary free left module is the direct sum of the right module.

    def equivalence : Tensor k A M (I →₀ A) ≃ₗ[k] (I →₀ M) where
    …

    Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

11. theorem OAI.LittleFinitistic.BalancedTensor.FreeLeft.evaluation_naturality line 82
12. theorem OAI.LittleFinitistic.BalancedTensor.FreeLeft.tensor_exact line 100

    Source documentation

    Free left tensor preserves exact sequences of right modules.

    theorem tensor_exact (f : M →ₗ[Aᵐᵒᵖ] M') (g : M' →ₗ[Aᵐᵒᵖ] M'')
        (h : Function.Exact f g) :
        Function.Exact (mapLeft (k := k) (I →₀ A) f) (mapLeft (k := k) (I →₀ A) g) := by
    …

    Mentions: OAI.LittleFinitistic.BalancedTensor.mapLeft