map_injective — Mathlib

English

If F is a faithful functor, then F maps morphisms injectively, i.e., different arrows map to different arrows.

Русский

Если F верный функтор, то отображение стрел F.map инъективно, то есть различные стрелки отображаются в различные стрелки.

LaTeX

$$$\\operatorname{Faithful} F \\Rightarrow \\operatorname{Injective}(F.map)$$$

Lean4

theorem map_injective (F : C ⥤ D) [Faithful F] : Function.Injective <| (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  Faithful.map_injective

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