isoWhiskerRight_twice — Mathlib

English

The isomorphism isoWhiskerRight (isoWhiskerRight α F) G equals a composite built from associators and isoWhiskerRight α (F ⋙ G) and the associator inverse.

Русский

Изоморфизм isoWhiskerRight (isoWhiskerRight α F) G равен композиции через ассоциаторы и isoWhiskerRight α (F ⋙ G) и обратный ассоциатор.

LaTeX

$$$\\mathrm{isoWhiskerRight}(\\mathrm{isoWhiskerRight}\\;α\\;F)\\;G = \\mathrm{Functor.associator}\\,\\_\\_\\_ \\; ≪≫ \\; \\mathrm{isoWhiskerRight}\\;α\\,(F\\circ G) \\;≪≫ (\\mathrm{Functor.associator}\\;\\_\\_\\_).symm$$$

Lean4

@[simp, reassoc]
theorem isoWhiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ≅ K) :
    isoWhiskerRight (isoWhiskerRight α F) G =
      Functor.associator _ _ _ ≪≫ isoWhiskerRight α (F ⋙ G) ≪≫ (Functor.associator _ _ _).symm :=
  by cat_disch

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