partialRightAdjointHomEquiv — Mathlib

English

There is a canonical bijection (X ⟶ F.partialRightAdjointObj Y) ≃ (F.obj X ⟶ Y.obj).

Русский

Существует каноническая биекция (X ⟶ F.partialRightAdjointObj Y) ≃ (F.obj X ⟶ Y.obj).

LaTeX

$$$(X \to F.partialRightAdjointObj Y) \cong (F.obj X \to Y.obj)$$$

Lean4

/-- Given `F : C ⥤ D`, this is the canonical bijection
`(X ⟶ F.partialRightAdjointObj Y) ≃ (F.obj X ⟶ Y.obj)`
for all `X : C` and `Y : F.PartialRightAdjointSource`. -/
noncomputable def partialRightAdjointHomEquiv {X : C} {Y : F.PartialRightAdjointSource} :
    (X ⟶ F.partialRightAdjointObj Y) ≃ (F.obj X ⟶ Y.obj) :=
  (F.op ⋙ yoneda.obj Y.obj).representableBy.homEquiv

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