map₂_id — Mathlib

English

For any F in YonedaCollection, the map₂ operation sends the identity morphism on X to the identity morphism on X.

Русский

Для любого F из YonedaCollection операция map₂ отправляет тождественный морфизм на X в тождественный морфизм на X.

LaTeX

$$$$\text{YonedaCollection.map₂ }F(\mathrm{Id}_X) = \mathrm{id}.$$$$

Lean4

@[simp]
theorem map₂_id : YonedaCollection.map₂ F (𝟙 X) = id := by ext; all_goals simp

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