English
Let K and L be coverages on C and P a presheaf. The isomorphism between the IsSheaf condition for the union of K and L and the pair of IsSheaf conditions for K and L separately holds, mirroring the previous isSheaf_sup result.
Русский
Пусть K и L — покрытия на C и P — предобразная функция. Аналогично предыдущему результату isSheaf_sup, условие isSheaf для объединения совпадает с и условиями для каждого покрытия отдельно.
LaTeX
$$$(\\mathrm{IsSheaf}((K \\sqcup L).\\mathrm{toGrothendieck})P) \\iff (\\mathrm{IsSheaf}(K.toGrothendieck)P) \\land (\\mathrm{IsSheaf}(L.toGrothendieck)P)$$$
Lean4
theorem isSheaf_sup (K L : Coverage C) (P : Cᵒᵖ ⥤ D) :
(IsSheaf (K ⊔ L).toGrothendieck) P ↔ (IsSheaf K.toGrothendieck) P ∧ (IsSheaf L.toGrothendieck) P :=
⟨fun h ↦ ⟨fun E ↦ ((Presieve.isSheaf_sup K L _).mp (h E)).1, fun E ↦ ((Presieve.isSheaf_sup K L _).mp (h E)).2⟩,
fun ⟨h₁, h₂⟩ E ↦ (Presieve.isSheaf_sup K L _).mpr ⟨h₁ E, h₂ E⟩⟩
