eq_mk_of_comm — Mathlib

English

If there is an isomorphism i: A ≅ X with i.hom ≫ X.arrow = f, then X = mk f.

Русский

Если есть изоморфизм i: A ≅ X и i.hom ≫ X.arrow = f, то X = mk f.

LaTeX

$$$\\text{If } i: A \\cong X,\\; i.hom \\;\\gg\\; X.arrow = f, \\;\\text{then } X = mk f$$$

Lean4

/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows. -/
theorem eq_mk_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : (X : C) ≅ A) (w : i.hom ≫ f = X.arrow) :
    X = mk f :=
  eq_of_comm (i.trans (underlyingIso f).symm) <| by simp [w]

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