whiskerRight_id — Mathlib

English

For f: X → Y, whiskering on the right by the unit object yields f ▷ 𝟙_C = (ρ_X).hom ≫ f ≫ (ρ_Y).inv, where ρ is the right unitor.

Русский

Для f: X → Y правое обёртывание единицей даёт f ▷ 𝟙_C = (ρ_X).hom ≫ f ≫ (ρ_Y).inv, где ρ — правый унитор.

LaTeX

$$$ f \\triangleleft \\mathbf{1}_C = (\\rho_X).hom \\circ f \\circ (\\rho_Y).inv $$$

Lean4

@[reassoc, simp]
theorem whiskerRight_id {X Y : C} (f : X ⟶ Y) : f ▷ 𝟙_ C = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv := by
  rw [← assoc, ← rightUnitor_naturality]; simp

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