English
The op of whiskering on the right commutes with the op-construction: (op (whiskerRight α H)) = (hom of opComp) ∘ whiskerRight (op α) H.op ∘ (inv of opComp).
Русский
Операция взятия противоположности после правого whiskerRight совпадает с композицией противоположностей: ...
LaTeX
$$$\\\\forall {E: Type*} [\\\\text{Category } E] \\\\forall {H: D \\\\to E} \\\\forall {F G: C \\\\to D^{op}} \\\\forall (\\\\alpha: F \\\\to G), \\\\mathrm{NatIso}.op( whiskerRight\\\\alpha H) = (\\\\mathrm{Functor}.opComp _ _).hom \\\\circ whiskerRight (\\\\mathrm{NatTrans}.op\\\\alpha) H.op \\\\circ (\\\\mathrm{Functor}.opComp _ _).inv.$$$
Lean4
@[reassoc]
theorem op_whiskerRight {E : Type*} [Category E] {H : D ⥤ E} (α : F ⟶ G) :
NatTrans.op (whiskerRight α H) =
(Functor.opComp _ _).hom ≫ whiskerRight (NatTrans.op α) H.op ≫ (Functor.opComp _ _).inv :=
by cat_disch
