counitInv_functor_comp — Mathlib

English

A triangle identity involving counitInv and the functor.

Русский

Треугольное тождество, связанное с counitInv и функтором.

LaTeX

$$$e.counitInv.app X \\;\\circ \\;e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X)$$$

Lean4

@[reassoc (attr := simp)]
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) := by
  simpa using Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) (Iso.refl _)

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