The hom functor, sending (X, Y) to the type X ⟶ Y.
def
CategoryTheory.Functor.hom
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
CategoryTheory.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
@[simp]
theorem
CategoryTheory.Functor.hom_obj
(C : Type u)
[CategoryTheory.Category.{v, u} C]
(p : Cᵒᵖ × C)
:
(CategoryTheory.Functor.hom C).obj p = (Opposite.unop p.1 ⟶ p.2)
@[simp]
theorem
CategoryTheory.Functor.hom_map
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X✝ Y✝ : Cᵒᵖ × C}
(f : X✝ ⟶ Y✝)
(h : Opposite.unop X✝.1 ⟶ X✝.2)
:
(CategoryTheory.Functor.hom C).map f h = CategoryTheory.CategoryStruct.comp f.1.unop (CategoryTheory.CategoryStruct.comp h f.2)