English
Dual to the previous construction: given a natural equivalence e between Hom_D(F(X), Y) and Hom_C(X, G(Y)) with a compensating naturality law, we obtain an adjunction F ⊣ rightAdjointOfEquiv e.
Русский
Дубль к предыдущей конструкции: данная естественная эквивалентность между Hom_D(F(X), Y) и Hom_C(X, G(Y)) с соответствующим законом натуральности порождает адъюнкцию F ⊣ rightAdjointOfEquiv e.
LaTeX
$$$ F \dashv (rightAdjointOfEquiv\ e\ ) $$$
Lean4
/-- Show that the functor given by `rightAdjointOfEquiv` is indeed right adjoint to `F`. Dual
to `adjunctionOfEquivRight`. -/
@[simps!]
def adjunctionOfEquivRight (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) : F ⊣ (rightAdjointOfEquiv e he) :=
mkOfHomEquiv
{ homEquiv := e
homEquiv_naturality_left_symm := by intro X X' Y f g; rw [Equiv.symm_apply_eq]; simp [he]
homEquiv_naturality_right := by
intro X Y Y' g h
simp [← he, reassoc_of% (he'' e)] }
