isLimit_iff_isSheafFor_presieve — Mathlib

English

Two morphisms E → P(X) that agree after composing with all arrows from the cover are equal.

Русский

Две стрелки E → P(X), совпадающие после композиции с любыми стрелками покрытия, равны.

LaTeX

$$$e_1 = e_2 \\text{ if } \\forall I: S.Arrow, e_1 \\circ I.f = e_2 \\circ I.f$$$

Lean4

/-- Given presieve `R` and presheaf `P : Cᵒᵖ ⥤ A`, the natural cone associated to `P` and
    the sieve `Sieve.generate R` generated by `R` is a limit cone iff `Hom (E, P -)` is a
    sheaf of types for the presieve `R` and all `E : A`. -/
theorem isLimit_iff_isSheafFor_presieve :
    Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op)) ↔ ∀ E : Aᵒᵖ, IsSheafFor (P ⋙ coyoneda.obj E) R :=
  (isLimit_iff_isSheafFor P _).trans (forall_congr' fun _ => (isSheafFor_iff_generate _).symm)

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