isSheaf_functorEnrichedHom — Mathlib

English

If F,G are presheaves on Cᵒᵖ valued in A with G a sheaf, then the presheaf of enriched Hom from F to G is a sheaf (under suitable Enriched Hom structure).

Русский

Если F,G — прешерфы на Cᵒᵖ со значениями в A, и G —Sheaf, то прешерф гомоморфизмов обогащённых из F в G является Sheaf.

LaTeX

$$Presheaf.IsSheaf J (functorEnrichedHom A F G)$$

Lean4

theorem isSheaf_functorEnrichedHom (F G : Cᵒᵖ ⥤ A) (hG : Presheaf.IsSheaf J G) [HasFunctorEnrichedHom A F G] :
    Presheaf.IsSheaf J (functorEnrichedHom A F G) := fun M ↦
  by
  rw [Presieve.isSheaf_iff_of_nat_equiv (functorEnrichedHomCoyonedaObjEquiv M F G)
      (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)]
  rw [← isSheaf_iff_isSheaf_of_type]
  exact Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

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