Theorems · Definition · category theory

CategoryTheory.Subobject.ofMkLE

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B A : C} →
      (f : A ⟶ B) →
        [inst_1 : CategoryTheory.Mono f] →
          (X : CategoryTheory.Subobject B) →
            CategoryTheory.Subobject.mk f ≤ X → (A ⟶ CategoryTheory.Subobject.underlying.obj X)

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

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Mono