eq_of_comp_arrow_eq — Mathlib

English

If two morphisms f,g: X → P into a subobject P have the same composite with the inclusion arrow P.arrow, then f = g.

Русский

Если две стрелки f,g: X → P имеют одинаковые композиции с стрелкой P.arrow, то f = g.

LaTeX

$$$f \\;\\circ P.arrow = g \\;\\circ P.arrow \\Rightarrow f = g$$$

Lean4

/-- Two morphisms into a subobject are equal exactly if
the morphisms into the ambient object are equal -/
@[ext]
theorem eq_of_comp_arrow_eq {X Y : C} {P : Subobject Y} {f g : X ⟶ P} (h : f ≫ P.arrow = g ≫ P.arrow) : f = g :=
  (cancel_mono P.arrow).mp h

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