Theorems · Definition · category theory

CategoryTheory.Under.homMk

{T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {U V : CategoryTheory.Under X} →
        (f : U.right ⟶ V.right) →
          autoParam (CategoryTheory.CategoryStruct.comp U.hom f = V.hom) CategoryTheory.Under.homMk._auto_1 → (U ⟶ V)

To give a morphism in the under category, it suffices to give a morphism fitting in a commutative triangle.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

43 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category