English
The unop of isoWhiskerRight α H equals the composition with unop α and unop H.
Русский
Обратная операция к isoWhiskerRight α H равна композиции с unop α и unop H.
LaTeX
$$$\\\\forall {C} [Category C], \\\\forall {D} [Category D], \\\\forall {F G : CategoryTheory.Functor C D}, \\\\forall {E} [Category E], \\\\forall {H : D \\\\to E}, \\\\mathrm{NatIso}.unop(\\\\mathrm{isoWhiskerRight} α H) = (\\\\mathrm{Functor}.unopComp _ _) \\\\llimes \\\\mathrm{isoWhiskerRight}(\\\\mathrm{NatIso}.unop α) H.unop \\\\llimes (\\\\mathrm{Functor}.unopComp _ _).symm.$$$
Lean4
theorem unop_whiskerRight {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category E] {H : Dᵒᵖ ⥤ Eᵒᵖ} (α : F ≅ G) :
NatIso.unop (isoWhiskerRight α H) =
(Functor.unopComp _ _) ≪≫ isoWhiskerRight (NatIso.unop α) H.unop ≪≫ (Functor.unopComp _ _).symm :=
by cat_disch
