English
Given a function e assigning to each X the isomorphism between Hom_D(F(X), Y) and Hom_C(X, G(Y)) that is natural in X and Y, and a law relating how e transforms under composition, one obtains an adjunction with left adjoint given by leftAdjointOfEquiv and right adjoint G.
Русский
Имея отображение e, задающее естественную изоморфность между Hom_D(F(X), Y) и Hom_C(X, G(Y)) и закон преобразования под композициями, можно получить адъюнкцию с левой частью leftAdjointOfEquiv и правой частью G.
LaTeX
$$$$ ext{leftAdjointOfEquiv}(e) \dashv G $$ with the naturality condition given in e$$
Lean4
/-- Construct a right adjoint functor to `F`, given the functor's value on objects `G_obj` and
a bijection `e` between `F.obj X ⟶ Y` and `X ⟶ G_obj Y` satisfying a naturality law
`he : ∀ X Y Y' g h, e X' Y (F.map f ≫ g) = f ≫ e X Y g`.
Dual to `leftAdjointOfEquiv`. -/
@[simps!]
def rightAdjointOfEquiv (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) : D ⥤ C
where
obj := G_obj
map {Y} {Y'} g := (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 _) ≫ g)
map_comp := fun {Y} {Y'} {Y''} g g' =>
by
rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_apply]
conv =>
rhs
rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
simp
