Theorems · Theorem · linear algebra

contractLeft_assoc_coevaluation

∀ (K : Type u) [inst : Field K] (V : Type v) [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V],
  LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ
      ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ
        LinearMap.lTensor (Module.Dual K V) (coevaluation K V) =
    ↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V))

This lemma corresponds to one of the coherence laws for duals in rigid categories, see CategoryTheory.Monoidal.Rigid.

Defined in

Mathlib.LinearAlgebra.Coevaluation

Cited by

0 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldAddCommGroupModuleFiniteDimensional