isSheaf_of_isSheaf_comp — Mathlib

English

Let J be a Grothendieck topology on C, A and B categories, and s: A → B a functor that reflects limits of a given size. If P is a presheaf Cᵒᵖ → A and P ⋙ s is a J-sheaf, then P is a J-sheaf.

Русский

Пусть J — топология Гротендикa на C, A, B — категории, а s: A → B — функтор, отражающий пределы некоторого размера. Если X — распр. предобозначение P: Cᵒᵖ → A и P ⋙ s является J-шейфом, то P сам является J-шейфом.

LaTeX

$$$IsSheaf(J, P \circ s) \Rightarrow IsSheaf(J, P)$$$

Lean4

theorem isSheaf_of_isSheaf_comp (s : A ⥤ B) [ReflectsLimitsOfSize.{v₁, max v₁ u₁} s] (h : IsSheaf J (P ⋙ s)) :
    IsSheaf J P := by
  rw [isSheaf_iff_isLimit] at h ⊢
  exact fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfReflects s t

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