isSheaf_comp_of_isSheaf — Mathlib

English

Let J be a Grothendieck topology on C, and s: A → B a functor with HasLimitsOfSize and PreservesLimitsOfSize, that reflects isomorphisms. For a presheaf P valued in A, P is a J-sheaf iff P ⋙ s is a J-sheaf.

Русский

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

LaTeX

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

Lean4

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

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