contractLeft_assoc_coevaluation'
theorem 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.lTensor V (contractLeft K V) ∘ₗ
↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) =
↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)
This theorem states that for any field `K` and any vector space `V` over `K` that is finite-dimensional, the composition of several specific linear maps is equal to the composition of two other specific linear maps. The maps involved are the left tensor of `V` with the contractLeft map of `K` and `V`, the association of `K`, `V`, the dual of `K` and `V`, and the right tensor of `V` with the coevaluation of `K` and `V` in the first composition. The second composition involves the symmetric of the right identity of the tensor product of `K` and `V` and the left identity of the tensor product of `K` and `V`. This theorem corresponds to one of the coherence laws for duals in rigid categories.
More concisely: For any finite-dimensional vector space V over a field K, the composition of the left tensor with contractLeft map, association map, dual, and right tensor with coevaluation, is equal to the composition of the symmetric of the right identity and left identity of the tensor product with the right identity and left identity of V.
|
contractLeft_assoc_coevaluation
theorem 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 theorem states that for any field `K` and a vector space `V` over `K` that is finite dimensional, the composition of several linear transformations, specifically the right tensor of the contract left function with the dual space of `V` over `K`, the inverse of the associative tensor product, and the left tensor of the coevaluation function with the dual space of `V` over `K`, is equivalent to the composition of the inverses of the left and right identity functions for the tensor product of modules, with the dual space of `V` over `K`. This law is one of the coherence laws for duals in rigid categories in category theory.
More concisely: For any finite-dimensional vector space `V` over a field `K`, the composition of the right tensor of the contract left function with the dual space, the inverse of the associative tensor product, and the left tensor of the coevaluation function with the dual space, equals the composition of the inverses of the left and right identity functions for the tensor product of `V` over `K`.
|