Tensor products of transports along object equalities

The tensor product of two morphisms eqToHom h and eqToHom h' is the transport along the induced equality of tensor products. This complements Mathlib's MonoidalCategory.whiskerLeft_eqToHom and MonoidalCategory.eqToHom_whiskerRight, which treat whiskering.

The inverse tensor comparison of an oplax monoidal functor F, followed by the image under F of a morphism out of a tensor product, is unchanged when the factors and the target are transported along object equalities. In particular, the inverse of an invertible tensor comparison δ F a b followed by F applied to a transport of a ⊗ b is the transport of F a ⊗ F b followed by the inverse tensor comparison at the transported factors.

Main results

• TauCeti.eqToHom_tensorHom_eqToHom: eqToHom h ⊗ₘ eqToHom h' = eqToHom _.
• CategoryTheory.Functor.eqToHom_conjugate_inv_δ_comp_map: transporting inv (δ F M N) ≫ F.map φ along equalities M = M', N = N' and P = P' gives inv (δ F M' N') ≫ F.map ψ, where ψ is the transport of φ;
• CategoryTheory.Functor.inv_δ_comp_map_eqToHom: transporting inv (δ F a b) along a = a' and b = b'.

@[simp]

theorem TauCeti.eqToHom_tensorHom_eqToHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y Y' : C} (h : X = X') (h' : Y = Y') : CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom h) (CategoryTheory.eqToHom h') = CategoryTheory.eqToHom ⋯

The tensor product of two transports along object equalities is the transport along the induced equality of tensor products.

theorem CategoryTheory.Functor.eqToHom_conjugate_inv_δ_comp_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {M M' N N' P P' : C} (hM : M = M') (hN : N = N') (hP : P = P') [IsIso (OplaxMonoidal.δ F M N)] [IsIso (OplaxMonoidal.δ F M' N')] (φ : MonoidalCategoryStruct.tensorObj M N ⟶ P) (ψ : MonoidalCategoryStruct.tensorObj M' N' ⟶ P') (hψ : ψ = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (eqToHom ⋯) (eqToHom ⋯)) (CategoryStruct.comp φ (eqToHom hP))) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (eqToHom ⋯) (eqToHom ⋯)) (CategoryStruct.comp (CategoryTheory.inv (OplaxMonoidal.δ F M' N')) (CategoryStruct.comp (F.map ψ) (eqToHom ⋯))) = CategoryStruct.comp (CategoryTheory.inv (OplaxMonoidal.δ F M N)) (F.map φ)

The inverse tensor comparison of an oplax monoidal functor F, followed by the image under F of a morphism φ : M ⊗ N ⟶ P, is unchanged when M, N and P are transported along object equalities: transporting φ to ψ : M' ⊗ N' ⟶ P' transports inv (δ F M N) ≫ F.map φ to inv (δ F M' N') ≫ F.map ψ.

theorem CategoryTheory.Functor.inv_δ_comp_map_eqToHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {a a' b b' : C} [IsIso (OplaxMonoidal.δ F a b)] [IsIso (OplaxMonoidal.δ F a' b')] (ha : a = a') (hb : b = b') (h : MonoidalCategoryStruct.tensorObj a b = MonoidalCategoryStruct.tensorObj a' b') : CategoryStruct.comp (CategoryTheory.inv (OplaxMonoidal.δ F a b)) (F.map (eqToHom h)) = CategoryStruct.comp (eqToHom ⋯) (CategoryTheory.inv (OplaxMonoidal.δ F a' b'))

The inverse tensor comparison of an oplax monoidal functor commutes with transports along identifications of the factors.

theorem CategoryTheory.Functor.inv_δ_comp_map_eqToHom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {a a' b b' : C} [IsIso (OplaxMonoidal.δ F a b)] [IsIso (OplaxMonoidal.δ F a' b')] (ha : a = a') (hb : b = b') (h : MonoidalCategoryStruct.tensorObj a b = MonoidalCategoryStruct.tensorObj a' b') {Z : D} (h✝ : F.obj (MonoidalCategoryStruct.tensorObj a' b') ⟶ Z) : CategoryStruct.comp (CategoryTheory.inv (OplaxMonoidal.δ F a b)) (CategoryStruct.comp (F.map (eqToHom h)) h✝) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (CategoryTheory.inv (OplaxMonoidal.δ F a' b')) h✝)

The inverse tensor comparison of an oplax monoidal functor commutes with transports along identifications of the factors.