Theorems · Definition · category theory

CategoryTheory.Over.homMk

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

To give a morphism in the over category, it suffices to give an arrow fitting in a commutative triangle.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

115 results in Mathlib

Foundations

Depth 28 from the axioms, rests on 142 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category