English
Unop commutes with whiskering on the left for natural isomorphisms: unop( whiskerLeft H α ) equals the corresponding expression with unop α.
Русский
Unop commute с левым whiskerLeft для нат изоморфизмов: unop( whiskerLeft H α ) = ...
LaTeX
$$$\\\\forall {F,G : C^{op} ⥤ D^{op}} {E} [Category E] {H : E^{op} ⥤ C^{op}} (α : F \\to G) : \\\\mathrm{NatIso}.unop(\\\\mathrm{isoWhiskerLeft} H α) = \\\\mathrm{Functor}.unopComp _ _ .\\\\hom \\\\circ whiskerLeft H.unop (\\\\mathrm{NatIso}.unop α) \\\\circ \\\\mathrm{Functor}.unopComp _ _ .\\\\inv.$$$
Lean4
@[reassoc]
theorem unop_whiskerLeft {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category E] {H : Eᵒᵖ ⥤ Cᵒᵖ} (α : F ⟶ G) :
NatTrans.unop (whiskerLeft H α) =
(Functor.unopComp _ _).hom ≫ whiskerLeft H.unop (NatTrans.unop α) ≫ (Functor.unopComp _ _).inv :=
by cat_disch
