unit_app_comp_inverse_map_η_functor

English

Duplicate of the unit-app-tensor-δ functor relation for the equivalence.

Русский

Дубликат соотношения единицы/тензора/δ для эквивалентности.

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 unit_app_comp_inverse_map_η_functor : e.unit.app (𝟙_ C) ≫ e.inverse.map (η e.functor) = ε e.inverse :=
  e.toAdjunction.unit_app_unit_comp_map_η

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