English
Let E, E' be categories and let F : Cᵒᵖ ⥤ Dᵒᵖ, G : Dᵒᵖ ⥤ Eᵒᵖ, H : Eᵒᵖ ⥤ E'ᵒᵖ be functors. Then NatIso.unop (Functor.associator F G H) equals a composite built from unop components and whiskers, i.e. NatIso.unop (Functor.associator F G H) = Functor.unopComp _ _ ≪≫ isoWhiskerLeft F.unop (Functor.unopComp _ _) ≪≫ (Functor.associator F.unop G.unop H.unop).symm ≪≫ isoWhiskerRight (Functor.unopComp _ _).symm H.unop ≪≫ (Functor.unopComp _ _).symm.
Русский
Пусть заданы категории E и E', а также F : Cᵒᵖ ⥤ Dᵒᵖ, G : Dᵒᵖ ⥤ Eᵒᵖ и H : Eᵒᵖ ⥤ E'ᵒᵖ. Тогда обратный ассоциатор равен композиции из соответствующих составляющих.
LaTeX
$$$\mathrm{NatIso.unop}(\mathrm{Functor.associator} F G H) = \mathrm{Functor.unopComp} \\_ \\_
\circ \mathrm{isoWhiskerLeft} F.unop (\mathrm{Functor.unopComp} \_ \_ )
\circ (\mathrm{Functor.associator} F.unop G.unop H.unop)^{-1}
\circ \mathrm{isoWhiskerRight}(\mathrm{Functor.unopComp} \_ \_).symm H.unop
\circ (\mathrm{Functor.unopComp} \_ \_ ).symm$$$
Lean4
theorem unop_associator {E E' : Type*} [Category E] [Category E'] {F : Cᵒᵖ ⥤ Dᵒᵖ} {G : Dᵒᵖ ⥤ Eᵒᵖ} {H : Eᵒᵖ ⥤ E'ᵒᵖ} :
NatIso.unop (Functor.associator F G H) =
Functor.unopComp _ _ ≪≫
isoWhiskerLeft F.unop (Functor.unopComp _ _) ≪≫
(Functor.associator F.unop G.unop H.unop).symm ≪≫
isoWhiskerRight (Functor.unopComp _ _).symm H.unop ≪≫ (Functor.unopComp _ _).symm :=
by cat_disch
