mapWhiskerLeft_id — Mathlib

English

Whiskering an identity morphism on the right leaves the identity morphism unchanged: mapWhiskerLeft H (𝟙 Fᵣ) = 𝟙.

Русский

Ослабление слева для тождественного перехода сохраняет тождественный морфизм: mapWhiskerLeft H (𝟙 Fᵣ) = 𝟙.

LaTeX

$$$ mapWhiskerLeft H (\mathbb{1} Fᵣ) = \mathbb{1} $$$

Lean4

@[simp]
theorem mapWhiskerLeft_id (H : C ⥤ E) (Fᵣ : D ⥤ E') : mapWhiskerLeft H (𝟙 Fᵣ) = 𝟙 _ := by cat_disch

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