op_rightUnitor — Mathlib

English

The opposite of the right unitor is given by a composite with rightUnitor and opId.

Русский

Противоположность правого унитора задаётся через композицию с rightUnitor и opId.

LaTeX

$$$\\\\forall {C} [Category C], \\\\forall {F : CategoryTheory.Functor C D}, \\\\text{NatIso}.op F.rightUnitor = F.op.rightUnitor.symm \\\\llimes \\\\mathrm{isoWhiskerLeft} F.op (\\\\mathrm{Functor}.opId D).symm \\\\llimes (\\\\mathrm{Functor}.opComp _ _).symm.$$$

Lean4

theorem op_rightUnitor :
    NatIso.op F.rightUnitor =
      F.op.rightUnitor.symm ≪≫ isoWhiskerLeft F.op (Functor.opId D).symm ≪≫ (Functor.opComp _ _).symm :=
  by cat_disch

Похожие утверждения