Theorems · Theorem · category theory

CategoryTheory.Subobject.mk_eq_mk_of_comm

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g] (i : A₁ ≅ A₂),
  CategoryTheory.CategoryStruct.comp i.hom g = f → CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g

To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

10 results in Mathlib

Foundations

Depth 43 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoCategoryTheory.Mono