map_injective_iff — Mathlib

English

For a faithful functor F, equality of images implies equality of original arrows: F.map f = F.map g implies f = g.

Русский

Для верного функторa F равенство образов означает равенство исходных стрелок: F.map f = F.map g ⇒ f = g.

LaTeX

$$$F.map f = F.map g \\Rightarrow f = g$$$

Lean4

theorem map_injective_iff (F : C ⥤ D) [Faithful F] {X Y : C} (f g : X ⟶ Y) : F.map f = F.map g ↔ f = g :=
  ⟨fun h => F.map_injective h, fun h => by rw [h]⟩

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