forget₂_faithful — Mathlib

English

The forget₂ functor forget₂ C D is faithful, i.e., it reflects distinct morphisms: if two morphisms have the same underlying map, they are equal only if they were equal to begin with.

Русский

Забывающий функтор forget₂ C D верен, то есть различия морфизмов отражаются по их базовым отображениям: если два морфизма имеют одинаковое подлежащее отображение, то они равны тогда и только тогда, когда были равны изначально.

LaTeX

$$$(forget₂ C D).Faithful$$$

Lean4

instance forget₂_faithful (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C] [Category.{v'} D]
    [HasForget.{w} D] [HasForget₂ C D] : (forget₂ C D).Faithful :=
  HasForget₂.forget_comp.faithful_of_comp

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