English
For an isomorphism α: F ≅ G of functors F,G: C → D, the opposite of isoWhiskerLeft α H equals the composition with op components and the op of α.
Русский
Для изоморфизма α: F ≅ G между функторaми F,G: C → D противоположная isoWhiskerLeft α H равна композиции через op-компоненты и op α.
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}.op(\\\\mathrm{isoWhiskerLeft} H α) = (\\\\mathrm{Functor}.opComp _ _) \\\\llimes \\\\mathrm{isoWhiskerLeft}(\\\\mathrm{NatIso}.op α) H.op \\\\llimes (\\\\mathrm{Functor}.opComp _ _).symm.$$$
Lean4
theorem op_isoWhiskerLeft {E : Type*} [Category E] {H : E ⥤ C} (α : F ≅ G) :
NatIso.op (isoWhiskerLeft H α) =
(Functor.opComp _ _) ≪≫ isoWhiskerLeft H.op (NatIso.op α) ≪≫ (Functor.opComp _ _).symm :=
by cat_disch
