English
If K and L are two coverages on C, then a presheaf P is a sheaf for the Grothendieck topology generated by the union of K and L if and only if P is a sheaf for K and P is a sheaf for L.
Русский
Если на C две системы покрытий K и L, то для предобращения P быть она является sheaf для объединённой топологии, порождаемой объединением K и L, тогда и только тогда P является sheaf для K и P является sheaf для L.
LaTeX
$$$\\mathrm{IsSheaf}((K \\sqcup L)^{\\mathrm{Gro}})P \\iff \\mathrm{IsSheaf}(K^{\\mathrm{Gro}})P \\land \\mathrm{IsSheaf}(L^{\\mathrm{Gro}})P$$$
Lean4
/-- A presheaf is a sheaf for the Grothendieck topology generated by a union of coverages iff it is a
sheaf for the Grothendieck topology generated by each coverage separately.
-/
theorem isSheaf_sup (K L : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
(Presieve.IsSheaf (K ⊔ L).toGrothendieck) P ↔
(Presieve.IsSheaf K.toGrothendieck) P ∧ (Presieve.IsSheaf L.toGrothendieck) P :=
by
refine
⟨fun h ↦
⟨Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_left) h,
Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_right) h⟩,
fun h ↦ ?_⟩
rw [isSheaf_coverage, isSheaf_coverage] at h
rw [isSheaf_coverage]
intro X R hR
rcases hR with hR | hR
· exact h.1 R hR
· exact h.2 R hR
