English
If F ≅ F' via a natural isomorphism iso, then for any X ∈ C, Y ∈ D there is a natural equivalence between Hom_D(F X, Y) and Hom_D(F' X, Y) given by composing with iso.inv at X on the left and iso.hom at X on the left on elements of the hom-sets.
Русский
Если F и F' естественно изоморфны через изоморфизм iso, тогда существует естественная эквиваленция множеств гомоморфизмов между Hom_D(FX, Y) и Hom_D(F'X, Y), задаваемая слева через iso.inv и iso.hom.
LaTeX
$$$ (F.obj X \to Y) \simeq (F'.obj X \to Y) $ with explicit maps $f \mapsto iso^{-1}_X \circ f$ and $g \mapsto iso_X \circ g$$$
Lean4
/-- Construct a left adjoint functor to `G`, given the functor's value on objects `F_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' (h ≫ g) = e X Y h ≫ G.map g`.
Dual to `rightAdjointOfEquiv`. -/
@[simps!]
def leftAdjointOfEquiv (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g) : C ⥤ D
where
obj := F_obj
map {X} {X'} f := (e X (F_obj X')).symm (f ≫ e X' (F_obj X') (𝟙 _))
map_comp := fun f f' => by
rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]
conv =>
rhs
rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
simp
