mapBifunctorRightUnitor_hasMap — Mathlib

English

The symmetry between mapBifunctorRightUnitor and the opposite/unitor constructions yields an isomorphism between the two graded-object level objects, preserved by the functorial maps.

Русский

Симметрия между операциями mapBifunctorRightUnitor и противоположными конструкциями образует изоморфизм между соответствующими объектами градаций, сохраняемый отображениями функторов.

LaTeX

$$$ mapBifunctorRightUnitor F Y e p hp X \cong X$$$

Lean4

theorem mapBifunctorRightUnitor_hasMap : HasMap (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)) p :=
  CofanMapObjFun.hasMap _ _ _ (mapBifunctorRightUnitorCofanIsColimit F Y e p hp X)

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