The hom functor, sending `(X, Y)` to the type `X ⟶ Y`.

source
def CategoryTheory.Functor.hom (C : Type u) [Category.{v, u} C] :
Functor (C ᵒᵖ × C) (Type v)

`Functor.hom` is the hom-pairing, sending `(X, Y)` to `X ⟶ Y`, contravariant in `X` and covariant in `Y`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.Functor.hom_obj (C : Type u) [Category.{v, u} C] (p : C ᵒᵖ × C) :
(hom C).obj p = (Opposite.unop p.1 ⟶ p.2)
source
@[simp]
theorem CategoryTheory.Functor.hom_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C ᵒᵖ × C} (f : X✝ ⟶ Y✝) (h : Opposite.unop X✝.1 ⟶ X✝.2) :
(hom C).map f h = CategoryStruct.comp f.1.unop (CategoryStruct.comp h f.2)