counitIso_inv_app_tensor_comp_functor_map_δ_inverse

English

For X,Y in C, the unit at X⊗Y composed with e.inverse.map(δ e.functor X Y) equals the tensor of unit at X and at Y followed by μ on the inverse side.

Русский

Единица на X⊗Y, затем e.inverse.map(δ e.functor X Y), равно тензору единиц на X и Y, за которым следует μ на обратной стороне.

LaTeX

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

Lean4

@[reassoc]
theorem counitIso_inv_app_tensor_comp_functor_map_δ_inverse (X Y : C) :
    e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
        e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) =
      μ e.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y) :=
  by
  rw [← cancel_epi (δ e.functor _ _), Monoidal.δ_μ_assoc]
  apply e.inverse.map_injective
  simp [← cancel_epi (e.unitIso.hom.app (X ⊗ Y)), Functor.map_comp,
    unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc]

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