counit_app_functor — Mathlib

English

Describes how the inverse part of the equivalence transforms a map f.

Русский

Определяет, как обратная часть эквивалентности превращает отображение f.

LaTeX

$$$e.inverse.map (e.functor.map f) = e.unitInv.app X \\;\\circ \\; f \\;\\circ \\; e.unitInv.app Y$$$

Lean4

theorem counit_app_functor (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X) := by
  simpa using Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)) (f := e.counit.app _)

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