mapBifunctorLeftUnitor_naturality

English

There is a right unitor isomorphism for the map bifunctor on graded objects, giving an isomorphism between the object obtained by applying the right unitor and the original graded object X.

Русский

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

LaTeX

$$$ mapBifunctorRightUnitor F p X ((single_0 I).obj Y) \\cong X $$$

Lean4

@[reassoc]
theorem mapBifunctorLeftUnitor_naturality :
    mapBifunctorMapMap F p (𝟙 _) φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').hom =
      (mapBifunctorLeftUnitor F X e p hp Y).hom ≫ φ :=
  by
  rw [← cancel_mono (mapBifunctorLeftUnitor F X e p hp Y').inv, assoc, assoc, Iso.hom_inv_id, comp_id,
    mapBifunctorLeftUnitor_inv_naturality, Iso.hom_inv_id_assoc]

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