English
For each object X in C, the object F(X) corepresents the functor Y ↦ Hom_C(X, G(Y)) in D, with the corepresentation given by the hom-equivalence Hom_D(F(X), Y) ≅ Hom_C(X, G(Y)) via adj.homEquiv X Y.
Русский
Для каждого объекта X в C объект F(X) корепрезентирует функтор Y ↦ Hom_C(X, G(Y)) в D, и естественная изоморфность задаётся через гом-эквивалентность Hom_D(F(X), Y) ≅ Hom_C(X, G(Y)) посредством adj.homEquiv X Y.
LaTeX
$$$ \operatorname{Hom}_D(F(X),Y) \cong \operatorname{Hom}_C(X, G(Y)) $ (естественная инвариация, задаваемая $\operatorname{adj.homEquiv}(X,Y)$)$$
Lean4
/-- If `adj : F ⊣ G`, and `X : C`, then `F.obj X` corepresents `Y ↦ (X ⟶ G.obj Y)`. -/
@[simps]
def corepresentableBy (X : C) : (G ⋙ coyoneda.obj (Opposite.op X)).CorepresentableBy (F.obj X)
where
homEquiv := adj.homEquiv _ _
homEquiv_comp := by simp
