eq_of_comm — Mathlib

English

If there exists an isomorphism f: X ≅ Y between underlying objects of subobjects X,Y of B such that f.hom ≫ Y.arrow = X.arrow, then X = Y.

Русский

Если есть изоморфизм f: X ≅ Y между базовыми объектами подмножеств X и Y подпредмета B, удовлетворяющий f.hom ≫ Y.arrow = X.arrow, то X = Y.

LaTeX

$$$\\exists f: X \\cong Y, f.hom \\;\\gg\\; Y.arrow = X.arrow \\Rightarrow X = Y$$$

Lean4

/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows. -/
@[ext (iff := false)]
theorem eq_of_comm {B : C} {X Y : Subobject B} (f : (X : C) ≅ (Y : C)) (w : f.hom ≫ Y.arrow = X.arrow) : X = Y :=
  le_antisymm (le_of_comm f.hom w) <| le_of_comm f.inv <| f.inv_comp_eq.2 w.symm

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