functor_map_id — Mathlib

English

For any F: Discrete J ⥤ C and any endomorphism f : j ⟶ j in the discrete index, the map on endomorphisms sends f to the identity on F.obj j.

Русский

Для любого F: Discrete J ⥤ C и любого эндоморфизма f : j ⟶ j в дискретном индексе отображение функторной карты отправляет f в тождественный морфизм на F.obj j.

LaTeX

$$$F.map f = \\mathrm{id}_{F(i)}$$$

Lean4

@[simp]
theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F.map f = 𝟙 (F.obj j) :=
  by
  have h : f = 𝟙 j := by cat_disch
  rw [h]
  simp

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