instFaithfulUnderToUnder — Mathlib

English

If F is a faithful functor, then the projection functor from the structured-arrow category to the underlying category is faithful.

Русский

Если F — верный функтор, то канонический переходник из структуры-стрелки в базовую категорию является верным.

LaTeX

$$$\mathsf{Faithful}\big(\mathrm{toUnder}(X,F)\big)$$$

Lean4

instance (X : T) (F : D ⥤ T) [F.Faithful] : (toUnder X F).Faithful :=
  show (StructuredArrow.pre _ _ _).Faithful from inferInstance

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