isSheaf_iff_isSheaf_comp — Mathlib

English

Under suitable size and limit-preserving assumptions on s, IsSheaf J P is equivalent to IsSheaf J (P ⋙ s).

Русский

При подходящих условиях размера и сохранения пределов функтор s обеспечивает эквивалентность IsSheaf J P и IsSheaf J (P ⋙ s).

LaTeX

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

Lean4

theorem isSheaf_iff_isSheaf_comp (s : A ⥤ B) [HasLimitsOfSize.{v₁, max v₁ u₁} A]
    [PreservesLimitsOfSize.{v₁, max v₁ u₁} s] [s.ReflectsIsomorphisms] : IsSheaf J P ↔ IsSheaf J (P ⋙ s) :=
  by
  letI : ReflectsLimitsOfSize s := reflectsLimits_of_reflectsIsomorphisms
  exact ⟨isSheaf_comp_of_isSheaf J P s, isSheaf_of_isSheaf_comp J P s⟩

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