mk_eq_of_comm — Mathlib

English

If f: A → B is mono and i: A ≅ X with w: i.hom ≫ X.arrow = f, then X = mk f.

Русский

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

LaTeX

$$$X = mk f$ under the data $(i: A \\cong X, w: i.hom \\circ X.arrow = f)$$$

Lean4

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

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