instFaithfulOppositeOp — Mathlib

English

If F is faithful, then its opposite functor F.op is faithful as well.

Русский

Если F верен (faithful), то его противоположный функтор F^{op} тоже верен.

LaTeX

$$$\\\\forall C [\\\\text{Category}(C)], \\\\forall D [\\\\text{Category}(D)], \\\\forall F: C \\\\to D, \\\\text{Faithful}(F) \\\\Rightarrow \\\\text{Faithful}(F^{op}).$$$

Lean4

instance {F : C ⥤ D} [Faithful F] : Faithful F.op where
  map_injective h := Quiver.Hom.unop_inj <| by simpa using map_injective F (Quiver.Hom.op_inj h)

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