English
The hom-pairing is a bifunctor from Cᵒᵖ × C to Type, with Hom(p) = unop(p.1) ⟶ p.2 and map defined by pre- and post-composition.
Русский
Пара гомоморфизмов образует двунаправленный функтор из Cᵒᵖ × C в Type: Hom(p) = unop(p.1) ⟶ p.2 и отображение задаётся предварительным и постпостдействием.
LaTeX
$$$\mathrm{hom} : C^{op} \times C \to \mathbf{Type}$,\n\quad \mathrm{Hom}_{C}(p) = \mathrm{unop}(p_1) \to p_2,\n\quad \mathrm{Hom}_{C}(f,h) = f_1.unop \circ h \circ f_2$$$
Lean4
/-- `Functor.hom` is the hom-pairing, sending `(X, Y)` to `X ⟶ Y`, contravariant in `X` and
covariant in `Y`. -/
@[simps]
def hom : Cᵒᵖ × C ⥤ Type v where
obj p := unop p.1 ⟶ p.2
map f h := f.1.unop ≫ h ≫ f.2
