rightOpWhiskerRight — Mathlib

English

The right_op of whiskering on the right satisfies an explicit expression with rightOpComp and whiskerRight of α.rightOp.

Русский

Правая Opposite-операция при whiskerRight удовлетворяет явному выражению через rightOpComp и whiskerRight α.rightOp

LaTeX

$$$\\\\forall {E : Type*} [Category E] {H : D \\\\to E} (α : F \\\\to G) : \\\\mathrm{NatIso}.rightOp(\\\\mathrm{whiskerRight} α H) = \\\\mathrm{Functor}.rightOpComp G H .hom \\\\circ whiskerRight α.rightOp H.op \\\\circ (\\\\mathrm{Functor}.rightOpComp F H).inv.$$$

Lean4

@[reassoc]
theorem rightOpWhiskerRight {E : Type*} [Category E] {H : D ⥤ E} (α : F ⟶ G) :
    (whiskerRight α H).rightOp =
      (Functor.rightOpComp G H).hom ≫ whiskerRight α.rightOp H.op ≫ (Functor.rightOpComp F H).inv :=
  by cat_disch

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