counitInv_app_functor — Mathlib

English

Relates the counitInv and unit at X through the functor.

Русский

Связь counitInv и unit на X через функтор.

LaTeX

$$$e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)$$$

Lean4

theorem counitInv_app_functor (e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X) :=
  by
  symm
  simp only [id_obj, comp_obj, counitInv]
  rw [← Iso.app_inv, ← Iso.comp_hom_eq_id (e.counitIso.app _), Iso.app_hom, functor_unit_comp]
  rfl

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