partialLeftAdjointHomEquiv — Mathlib

English

There is a canonical bijection between morphisms from X to F.partialLeftAdjointObj Y and morphisms from X.obj to F.obj Y, given by the Yoneda-based representable functor.

Русский

Существует каноническая биекция между морфизмами X → F.partialLeftAdjointObj Y и X.obj → F.obj Y, задаваемая при помощи представляемого по Yoneda функторов.

LaTeX

$$$(X \to F.partialLeftAdjointObj\; Y) \cong (X.obj \to F.obj\; Y)$$$

Lean4

/-- Given `F : D ⥤ C`, this is the canonical bijection
`(F.partialLeftAdjointObj X ⟶ Y) ≃ (X.obj ⟶ F.obj Y)`
for all `X : F.PartialLeftAdjointSource` and `Y : D`. -/
noncomputable def partialLeftAdjointHomEquiv {X : F.PartialLeftAdjointSource} {Y : D} :
    (F.partialLeftAdjointObj X ⟶ Y) ≃ (X.obj ⟶ F.obj Y) :=
  (F ⋙ coyoneda.obj (op X.obj)).corepresentableBy.homEquiv

Похожие утверждения