mk_eq_mk_of_comm — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{mk } f = X$$$

Lean4

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

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