OAI/Algebra/Finitistic/Ordinary/OrdinaryFreeTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.BalancedTensor.Free.coefficientAction line 13

    Source documentation

    A right-regular coefficient acts on the left tensor factor by its unop.

    def coefficientAction : Aᵐᵒᵖ →ₗ[k] N →ₗ[k] N :=
…
  2. def OAI.LittleFinitistic.BalancedTensor.Free.evaluateBilinear line 17

    Source documentation

    Coordinate evaluation of a free right module tensor N.

    def evaluateBilinear : (I →₀ Aᵐᵒᵖ) →ₗ[k] N →ₗ[k] (I →₀ N) :=
…
  3. theorem OAI.LittleFinitistic.BalancedTensor.Free.evaluateBilinear_single line 20
  4. def OAI.LittleFinitistic.BalancedTensor.Free.evaluation line 25
  5. theorem OAI.LittleFinitistic.BalancedTensor.Free.evaluation_single line 36
  6. def OAI.LittleFinitistic.BalancedTensor.Free.insertion line 40
  7. theorem OAI.LittleFinitistic.BalancedTensor.Free.insertion_single line 44
  8. theorem OAI.LittleFinitistic.BalancedTensor.Free.evaluation_insertion line 49
  9. theorem OAI.LittleFinitistic.BalancedTensor.Free.insertion_evaluation line 56
  10. def OAI.LittleFinitistic.BalancedTensor.Free.equivalence line 71

    Source documentation

    The actual free balanced tensor, for arbitrary index sets and arbitrary modules N.

    def equivalence : Tensor k A (I →₀ Aᵐᵒᵖ) N ≃ₗ[k] (I →₀ N) where
…

    Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor