functor_map_μ_inverse_comp_counitIso_hom_app_tensor

English

For the inverse side of an equivalence, the map of μ together with counit on X⊗Y relates to δ and the unit morphisms at X and Y.

Русский

Для обратной стороны эквивалентности отображение μ в сочетании с counit на X⊗Y связано с δ и единичными отображениями на X и Y.

LaTeX

$$$e.functor.map(\\\\mu G X Y) \\\\circ e.counit.app(X \\otimes Y) = δ F _ _ \\\\circ (e.counit.app X \\\\otimes e.counit.app Y)$$$

Lean4

@[reassoc]
theorem functor_map_μ_inverse_comp_counitIso_hom_app_tensor (X Y : D) :
    e.functor.map (μ e.inverse X Y) ≫ e.counitIso.hom.app (X ⊗ Y) =
      δ e.functor _ _ ≫ (e.counitIso.hom.app X ⊗ₘ e.counitIso.hom.app Y) :=
  e.toAdjunction.map_μ_comp_counit_app_tensor X Y

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