whiskerLeft_naturality_comp — Mathlib

English

Let B and C be bicategories, with F,G,H : B ⥤ C and η : StrongTrans F G, θ : StrongTrans G H. For f : a' ⟶ G.obj a, g : a ⟶ b, h : b ⟶ c, a naturality identity with respect to left whiskering holds.

Русский

Пусть B и C — двоуровневые категории, F,G,H : B → C и η: StrongTrans F G, θ: StrongTrans G H. Для f : a' ⟶ G.obj a, g : a ⟶ b, h : b ⟶ c выполняется натуральность левого взвешивания.

LaTeX

$$$f \triangleleft (\theta.naturality (g \gg h)).hom \; ≔ \; f \triangleleft G.mapComp g h \; \Rightarrow \; \dots$$$

Lean4

@[reassoc (attr := simp), to_app]
theorem whiskerLeft_naturality_comp (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) :
    f ◁ (θ.naturality (g ≫ h)).hom ≫ f ◁ θ.app a ◁ H.mapComp g h =
      f ◁ G.mapComp g h ▷ θ.app c ≫
        f ◁ (α_ _ _ _).hom ≫
          f ◁ G.map g ◁ (θ.naturality h).hom ≫
            f ◁ (α_ _ _ _).inv ≫ f ◁ (θ.naturality g).hom ▷ H.map h ≫ f ◁ (α_ _ _ _).hom :=
  θ.toOplax.whiskerLeft_naturality_comp _ _ _

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