op_leftUnitor — Mathlib

English

The opposite of the left unitor is given by a specific composite involving leftOp and opId.

Русский

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

LaTeX

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

Lean4

theorem op_leftUnitor :
    NatIso.op F.leftUnitor =
      F.op.leftUnitor.symm ≪≫ isoWhiskerRight (Functor.opId C).symm F.op ≪≫ (Functor.opComp _ _).symm :=
  by cat_disch

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