isSheaf — Mathlib

English

If P is separated and every compatible family on a covering sieve has an amalgamation, then P is a sheaf.

Русский

Если P разделённа и любая совместимая семья на покрывающем сита имеет амальгамацию, то P — шейф.

LaTeX

$$IsSeparated(J, P) ∧ (∀ X S ∈ J X, ∀ x, x.Compatible → ∃ t, x.IsAmalgamation t) ⇒ IsSheaf(J, P)$$

Lean4

/-- If `P` is separated and every compatible family of elements of `P` for a covering
sieve has an amalgamation, `P` is a sheaf. -/
theorem isSheaf {P : Cᵒᵖ ⥤ Type w} (h : IsSeparated J P)
    (h' : ∀ X, ∀ S ∈ J X, ∀ x : FamilyOfElements P S.arrows, x.Compatible → ∃ t, x.IsAmalgamation t) : IsSheaf J P :=
  fun _ S hS ↦ (h S hS).isSheafFor <| h' _ S hS

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