rightOp_faithful — Mathlib

English

If F: C^{op} ⥤ D is faithful, then F.rightOp is faithful.

Русский

Если F: C^{op} ⥤ D верен, то F.rightOp верен.

LaTeX

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

Lean4

/-- If F is faithful then the right_op of F is also faithful. -/
instance rightOp_faithful {F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp where
  map_injective h := Quiver.Hom.op_inj (map_injective F (Quiver.Hom.op_inj h))

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