mapWhiskerRight_comp — Mathlib

English

A variant of mkNatTrans equality asserting that whiskered left/right parts reconstruct the original natural transformation.

Русский

Вариант равенства mkNatTrans: ослабления слева и справа восстанавливают исходное натуральное преобразование.

LaTeX

$$$ mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) = α $$$

Lean4

@[simp]
theorem mapWhiskerRight_comp {Fₗ : C ⥤ E} {Gₗ : C ⥤ E} {Hₗ : C ⥤ E} (α : Fₗ ⟶ Gₗ) (β : Gₗ ⟶ Hₗ) (H : D ⥤ E') :
    mapWhiskerRight (α ≫ β) H = mapWhiskerRight α H ≫ mapWhiskerRight β H := by cat_disch

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