unitIso_hom_app_tensor_comp_inverse_map_δ_functor

English

For X,Y in C, the unitIso hom at X⊗Y composed with the inverse map of δ for the functor equals the unit morphisms at X and Y composed with μ on the inverse side.

Русский

Для X, Y в C, гом-под единицы на X⊗Y композицией через e.inverse.map(δ functor X Y) равна μ e.inverse соед. с единицами на X и Y.

LaTeX

$$$e.unitIso.hom.app(X \\otimes Y) \\\\circ e.inverse.map(\\\\delta e.functor X Y) = (e.unitIso.hom.app X \\\\otimes e.unitIso.hom.app Y) \\\\circ μ e.inverse _ _$$$

Lean4

@[reassoc]
theorem unitIso_hom_app_tensor_comp_inverse_map_δ_functor (X Y : C) :
    e.unitIso.hom.app (X ⊗ Y) ≫ e.inverse.map (δ e.functor X Y) =
      (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y) ≫ μ e.inverse _ _ :=
  e.toAdjunction.unit_app_tensor_comp_map_δ X Y

Похожие утверждения