op_whiskerLeft — Mathlib

English

Taking unop commutes with left whiskering: unop( whiskerLeft H α ) equals the corresponding expression with unop.

Русский

Слева от whiskerLeft пропускается операция unop и выражение эквивалентно с использованием unop.

LaTeX

$$$\\\\forall {H : E \\ to C} \\\\forall {F G: C^{op} ⥤ D^{op}} \\\\forall (α: F \\to G): \\\\mathrm{NatTrans}.unop(\\\\mathrm{whiskerLeft} H α) = \\\\mathrm{Functor}.unopComp _ _ .hom \\\\circ whiskerLeft H.unop (\\\\mathrm{NatTrans}.unop α) \\\\circ (\\\\mathrm{Functor}.unopComp _ _).inv.$$$

Lean4

@[reassoc]
theorem op_whiskerLeft {E : Type*} [Category E] {H : E ⥤ C} (α : F ⟶ G) :
    NatTrans.op (whiskerLeft H α) =
      (Functor.opComp _ _).hom ≫ whiskerLeft H.op (NatTrans.op α) ≫ (Functor.opComp _ _).inv :=
  by cat_disch

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