natIsoFunctor — Mathlib

English

Let F,G be functors Discrete I ⥤ C and f i : F.obj i ≅ G.obj i a family of isomorphisms. Then the app component of the natural isomorphism Discrete.natIso f at i equals f i.

Русский

Пусть F,G — функторы Discrete I ⥤ C и f i : F.obj i ≅ G.obj i — семейство изоморфизмов. Тогда компонент app естественной изоморфности Discrete.natIso f в i равен f i.

LaTeX

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

Lean4

/-- Every functor `F` from a discrete category is naturally isomorphic (actually, equal) to
  `Discrete.functor (F.obj)`. -/
@[simps!]
def natIsoFunctor {I : Type u₁} {F : Discrete I ⥤ C} : F ≅ Discrete.functor (F.obj ∘ Discrete.mk) :=
  natIso fun _ => Iso.refl _

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