English
A coherence identity for duals in a rigid category; a certain composition of lTensor, rTensor, coevaluation, and associator equals another canonical map.
Русский
Коэрцентная согласованность дуал в жесткой категории: композиции отображений совпадают.
LaTeX
$$((contractLeft K V).rTensor _ ) ∘ (TensorProduct.assoc K _ _ _).symm ∘ (coevaluation K V).lTensor (Module.Dual K V) = (TensorProduct.lid K _).symm ∘ (TensorProduct.rid K _).toLinearMap.$$
Lean4
/-- This lemma corresponds to one of the coherence laws for duals in rigid categories, see
`CategoryTheory.Monoidal.Rigid`. -/
theorem contractLeft_assoc_coevaluation :
(contractLeft K V).rTensor _ ∘ₗ
(TensorProduct.assoc K _ _ _).symm.toLinearMap ∘ₗ (coevaluation K V).lTensor (Module.Dual K V) =
(TensorProduct.lid K _).symm.toLinearMap ∘ₗ (TensorProduct.rid K _).toLinearMap :=
by
letI := Classical.decEq (Basis.ofVectorSpaceIndex K V)
apply TensorProduct.ext
apply (Basis.ofVectorSpace K V).dualBasis.ext; intro j; apply LinearMap.ext_ring
rw [LinearMap.compr₂_apply, LinearMap.compr₂_apply, TensorProduct.mk_apply]
simp only [LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_toLinearMap]
rw [rid_tmul, one_smul, lid_symm_apply]
simp only [LinearMap.lTensor_tmul, coevaluation_apply_one]
rw [TensorProduct.tmul_sum, map_sum]; simp only [assoc_symm_tmul]
rw [map_sum]; simp only [LinearMap.rTensor_tmul, contractLeft_apply]
simp only [Basis.coe_dualBasis, Basis.coord_apply, Basis.repr_self_apply, TensorProduct.ite_tmul]
rw [Finset.sum_ite_eq']; simp only [Finset.mem_univ, if_true]
