English
Similarly, if G ≅ G' via a natural isomorphism iso, then for any X ∈ C, Y ∈ D there is an equivalence between Hom(X, G Y) and Hom(X, G' Y) given by composing with iso.hom at Y on the right and iso.inv on the right.
Русский
Аналогично, если G ≅ G' естественно изоморфны через изоморфизм iso, существует эквивалентность между Hom(X, G Y) и Hom(X, G' Y), задаваемая правой композиции с iso.hom и iso.inv.
LaTeX
$$$ (X \to G.obj Y) \simeq (X \to G'.obj Y) $ via $f \mapsto f \circ iso.hom_Y$ and $g \mapsto g \circ iso.inv_Y$$$
Lean4
/-- Show that the functor given by `leftAdjointOfEquiv` is indeed left adjoint to `G`. Dual
to `adjunctionOfRightEquiv`. -/
@[simps!]
def adjunctionOfEquivLeft : leftAdjointOfEquiv e he ⊣ G :=
mkOfHomEquiv
{ homEquiv := e
homEquiv_naturality_left_symm := fun {X'} {X} {Y} f g =>
by
have {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') : (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g := by
rw [Equiv.symm_apply_eq, he]; simp
simp [← this, ← he] }
