mathlib documentation

category_theory.hom_functor

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

source
def category_theory.functor.hom (C : Type u) [category_theory.category C] :
Cᵒᵖ × C ⥤ Type v

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

Equations
source
@[simp]
theorem category_theory.functor.hom_obj (C : Type u) [category_theory.category C] (X : Cᵒᵖ × C) :
(category_theory.functor.hom C).obj X = (opposite.unop X.fst ⟶ X.snd)
source
@[simp]
theorem category_theory.functor.hom_pairing_map (C : Type u) [category_theory.category C] {X Y : Cᵒᵖ × C} (f : X ⟶ Y) :
(category_theory.functor.hom C).map f = λ (h : (category_theory.functor.hom C).obj X), f.fst.unop ≫ h ≫ f.snd