English
If F preserves a specified product along X, then F is a sheaf for the presieve of arrows associated to the disjoint coproduct X.
Русский
Если F сохраняет заданный произведение над X, то F является sheaf для презыва стрелок, связанных с дизъюнктивным копроductом X.
LaTeX
$$$ [\text{Presheaf.IsSheafFor } F] \quad \text{for } (\text{ofArrows } X c.inj) \text{ given } F \text{ preserves the product}$$$
Lean4
/-- If `F` preserves a particular product, then it `IsSheafFor` the corresponding presieve of arrows.
-/
theorem isSheafFor_of_preservesProduct [PreservesLimit (Discrete.functor (fun x ↦ op (X x))) F] :
(ofArrows X c.inj).IsSheafFor F :=
by
rw [Equalizer.Presieve.Arrows.sheaf_condition, Limits.Types.type_equalizer_iff_unique]
have : HasCoproduct X := ⟨⟨c, hc⟩⟩
have hi : IsIso (piComparison F (fun x ↦ op (X x))) := inferInstance
rw [piComparison_fac (hc := hc), isIso_iff_bijective, Function.bijective_iff_existsUnique] at hi
intro b _
obtain ⟨t, ht₁, ht₂⟩ := hi b
refine ⟨F.map ((opCoproductIsoProduct' hc (productIsProduct _)).inv) t, ht₁, fun y hy ↦ ?_⟩
apply_fun F.map ((opCoproductIsoProduct' hc (productIsProduct _)).hom) using injective_of_mono _
simp [← FunctorToTypes.map_comp_apply,
ht₂ (F.map ((opCoproductIsoProduct' hc (productIsProduct _)).hom) y) (by simp [← hy])]
