whiskerRight_id — Mathlib

English

For any G: C ⥤ D and F: D ⥤ E, whiskering the identity transformation on G with F yields the identity on G ⋙ F. In symbols, whiskerRight (NatTrans.id G) F = NatTrans.id (G.comp F).

Русский

Для любого G: C ⥤ D и F: D ⥤ E отбивка по F тождества на G даёт тождественный преобразователь на G ⋙ F: whiskerRight (NatTrans.id G) F = NatTrans.id (G ∘ F).

LaTeX

$$$\\operatorname{whiskerRight}(\\mathrm{NatTrans.id}\\,G)\\,F = \\mathrm{NatTrans.id}\\,(G\\circ F).$$$

Lean4

@[simp]
theorem whiskerRight_id {G : C ⥤ D} (F : D ⥤ E) : whiskerRight (NatTrans.id G) F = NatTrans.id (G.comp F) :=
  ((whiskeringRight C D E).obj F).map_id _

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