English
The unop of isoWhiskerLeft α H equals the composition with unop α and unop H.
Русский
Обратная операция к isoWhiskerLeft α 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 : E \\to C}, \\\\mathrm{NatIso}.unop(\\\\mathrm{isoWhiskerLeft} H α) = (\\\\mathrm{Functor}.unopComp _ _) \\\\llimes \\\\mathrm{whiskerLeft} H.unop (\\\\mathrm{NatIso}.unop α) \\\\llimes (\\\\mathrm{Functor}.unopComp _ _).symm.$$$
Lean4
theorem unop_whiskerLeft {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category E] {H : Eᵒᵖ ⥤ Cᵒᵖ} (α : F ≅ G) :
NatIso.unop (isoWhiskerLeft H α) =
(Functor.unopComp _ _) ≪≫ isoWhiskerLeft H.unop (NatIso.unop α) ≪≫ (Functor.unopComp _ _).symm :=
by cat_disch
