The hom functor, sending (X, Y) to the type X ⟶ Y.
@[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)
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.