functor_map — Mathlib

English

Given a family of isomorphisms f_i : F(i) ≅ G(i), the app component of the corresponding natural isomorphism equals f_i.

Русский

Пусть дано семейство изоморфизмов f_i : F(i) ≅ G(i); компонента приложения натурального изоморфизма равна f_i.

LaTeX

$$$(\\mathrm{Discrete.natIso}\\; f).\\mathrm{app}\\ i = f_i$$$

Lean4

theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) : (Discrete.functor F).map f = 𝟙 (F i.as) :=
  by cat_disch

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