mathlib3 documentation

category_theory.functor.hom

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] (p : Cᵒᵖ × C) :
(category_theory.functor.hom C).obj p = (opposite.unop p.fst ⟶ p.snd)
source
@[simp]
theorem category_theory.functor.hom_map (C : Type u) [category_theory.category C] (X Y : Cᵒᵖ × C) (f : X ⟶ Y) (h : opposite.unop X.fst ⟶ X.snd) :
(category_theory.functor.hom C).map f h = f.fst.unop ≫ h ≫ f.snd