isSheaf_of_le

Mathlib.CategoryTheory.Sites.SheafOfTypes

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.isSheaf_of_le

English

If J1 ≤ J2 and P is a J2-sheaf, then P is J1-sheaf.

Русский

Если J1 ≤ J2 и P — J2-шейф, то P — J1-шейф.

LaTeX

$$$J_1 \le J_2 \Rightarrow IsSheaf(J_2, P) \Rightarrow IsSheaf(J_1, P)$$$

Lean4

theorem isSheaf_of_le (P : Cᵒᵖ ⥤ Type w) {J₁ J₂ : GrothendieckTopology C} : J₁ ≤ J₂ → IsSheaf J₂ P → IsSheaf J₁ P :=
  fun h t _ S hS => t S (h _ hS)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru