freeYonedaHomEquiv — Mathlib

English

The bijection between morphisms freeYoneda J X M → F and M → F.val.obj(op X) for sheaves F.

Русский

Существует биекция между морфизмами freeYoneda J X M → F и M → F.val.obj(op X) для Sheaf F.

LaTeX

$$$(\text{freeYonedaHomEquiv}) : (freeYoneda J X M \to F) \simeq (M \to F.{val}.obj(op X))$$$

Lean4

/-- The bijection `(Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X))`
when `F : Sheaf J A`, `X : C` and `M : A`. -/
noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} :
    (freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X)) :=
  ((sheafificationAdjunction J A).homEquiv _ _).trans Presheaf.freeYonedaHomEquiv

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