comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom

English

There is a natural equivalence (bijective correspondence) between morphisms from the sheafification to F and morphisms from M0 to the restricted scalars of F.

Русский

Существует естественная эквиваленция между морфизмами от шейфификации к F и морфизмами из M0 в ограниченные скаляры F.

LaTeX

$$$sheafifyHomEquiv(\alpha, \varphi): ((\text{sheafify } α φ) ⟶ F) \simeq (M_0 ⟶ (\restrictScalars α).obj F).$$$

Lean4

theorem comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom {F : PresheafOfModules.{v} R.val}
    (hF : Presheaf.IsSheaf J F.presheaf) (f : M₀ ⟶ (restrictScalars α).obj F) :
    φ ≫ (toPresheaf R.val).map ((sheafifyHomEquiv' α φ hF).symm f) = (toPresheaf R₀).map f :=
  (toPresheaf _).congr_map ((sheafifyHomEquiv' α φ hF).apply_symm_apply f)

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