whiskerRight_id' — Mathlib

English

For any G: C ⥤ D and F: D ⥤ E, whiskering the identity on G with F yields the identity on G ⋙ F. This is the prime version of the identity under whiskering.

Русский

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

LaTeX

$$$\\text{whiskerRight}(\\mathbf{1}_G)\\,F = \\mathbf{1}_{G\\circ F}.$$$

Lean4

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

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