objMap_id — Mathlib

English

The map of an identity morphism is the identity on the corresponding intermediate object.

Русский

Отображение по объекту для тождественного морфизма даёт тождество на соответствующем промежуточном объекте.

LaTeX

$$objMap I κ (𝟙 f) = 𝟙 _$$

Lean4

@[simp]
theorem objMap_id (f : Arrow C) : objMap I κ (𝟙 f) = 𝟙 _ :=
  by
  simp only [objMap, Functor.map_id]
  rfl

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