whiskerRight_app_apply — Mathlib

English

The right whiskering coherently acts on a morphism f: K.functorHom L ⊗ L.functorHom M ⟶ K.functorHom M by sending x to pair (x.app, f.app).

Русский

Правое взвешивание по модулю морфизма f: K.functorHom L ⊗ L.functorHom M ⟶ K.functorHom M действует объединяя элементы как пару (x.app, f.app).

LaTeX

$$$(f \▷ M.functorHom N).app X a = \langle f.app X a.1, a.2 \rangle$$$

Lean4

@[simp]
theorem whiskerRight_app_apply (K L M N : C ⥤ D) (f : K.functorHom L ⊗ L.functorHom M ⟶ K.functorHom M) {X : C}
    (a : ((K.functorHom L ⊗ L.functorHom M) ⊗ M.functorHom N).obj X) :
    (f ▷ M.functorHom N).app X a = ⟨f.app X a.1, a.2⟩ :=
  rfl

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