Theorems · Definition · category theory

CategoryTheory.Subobject.ofLE

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

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

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

38 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category