isSheafFor_iff_preservesProduct — Mathlib

English

For X, c.inj representing a disjoint coproduct, F is IsSheafFor for the arrows presieve iff F preserves the corresponding product limit.

Русский

Для дизъюнктивного копроductа X и сопутствующей inj, IsSheafFor F относительно презив стрелок эквивалентно сохранению соответствующего предельного произведения.

LaTeX

$$$ (\text{ofArrows } X \; c.inj).IsSheafFor F \iff \text{PreservesLimit}(\mathrm{Discrete}(X), F)$$$

Lean4

theorem isSheafFor_iff_preservesProduct :
    (ofArrows X c.inj).IsSheafFor F ↔ PreservesLimit (Discrete.functor (fun x ↦ op (X x))) F :=
  ⟨fun hF' ↦ preservesProduct_of_isSheafFor _ hF hI c hc hd hF', fun _ ↦ isSheafFor_of_preservesProduct F c hc⟩

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