Theorems · Definition · category theory

CategoryTheory.Subobject.ofMkLEMk

{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] → CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g → (A₁ ⟶ A₂)

An inequality of subobjects is witnessed by some morphism between the corresponding objects.

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoCategoryTheory.Mono