English
For an adjunction F ⊣ G, there is a natural equivalence (F X → Y) ≃ (X → G Y) given by mapping f to unit_X followed by G f and inverse by F g followed by counit_Y.
Русский
Для сопряжённости F ⊣ G существует естественная биекция (F X → Y) ≃ (X → G Y), задаваемая f ↦ unit_X ; G f и обратная карта g ↦ F g ; counit_Y.
LaTeX
$$$(F \dashv G).homEquiv : (F.X \to Y) \simeq (X \to G.Y)$, с явно заданной формой: toFun f = unit_X ≫ G.map f, invFun g = F.map g ≫ counit_Y.$$
Lean4
/-- The hom set equivalence associated to an adjunction. -/
@[simps -isSimp]
def homEquiv {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) (X : C) (Y : D) : (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
where
toFun := fun f => adj.unit.app X ≫ G.map f
invFun := fun g => F.map g ≫ adj.counit.app Y
left_inv := fun f => by
dsimp
rw [F.map_comp, assoc, ← Functor.comp_map, adj.counit.naturality, ← assoc]
simp
right_inv := fun g => by
simp only [Functor.comp_obj, Functor.map_comp]
rw [← assoc, ← Functor.comp_map, ← adj.unit.naturality]
simp
