faithful — Mathlib

English

In the InducedWideCategory construction, the induced functor wideInducedFunctor F P : InducedWideCategory D F P ⥤ D is faithful; i.e., it reflects equality of morphisms.

Русский

В конструировании InducedWideCategory индуцируемый функтор wideInducedFunctor F P: InducedWideCategory D F P ⥤ D является верным; то есть он отображает равенство мортов полностью.

LaTeX

$$$\\operatorname{Faithful}((\\mathrm{wideInducedFunctor}\\;F\\;P))$$$

Lean4

/-- The induced functor `wideInducedFunctor F P : InducedWideCategory D F P ⥤ D`
is faithful. -/
instance faithful : (wideInducedFunctor F P).Faithful where
  map_injective {X Y} f g
    eq := by
    cases f
    cases g
    aesop

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