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