English
If F preserves the product over X, then the limit of the discrete diagram X is preserved by F, i.e., F(∏ X) ≅ ∏ F(X).
Русский
Если F сохраняет произведение над X, то предел дискретного диаграммы X сохраняется F, то есть F(∏ X) ≅ ∏ F(X).
LaTeX
$$$\mathrm{PreservesLimit}(\mathrm{Discrete}(X), F)$$$
Lean4
/-- If `F` is a presheaf which `IsSheafFor` a presieve of arrows and the empty presieve, then it
preserves the product corresponding to the presieve of arrows.
-/
theorem preservesProduct_of_isSheafFor (hF' : (ofArrows X c.inj).IsSheafFor F) :
PreservesLimit (Discrete.functor (fun x ↦ op (X x))) F :=
by
have : HasCoproduct X := ⟨⟨c, hc⟩⟩
refine @PreservesProduct.of_iso_comparison _ _ _ _ F _ (fun x ↦ op (X x)) _ _ ?_
rw [piComparison_fac (hc := hc)]
refine IsIso.comp_isIso' inferInstance ?_
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique]
rw [Equalizer.Presieve.Arrows.sheaf_condition, Limits.Types.type_equalizer_iff_unique] at hF'
exact fun b ↦ hF' b (congr_fun (firstMap_eq_secondMap F hF hI c hd) b)
