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