English
For type-valued presheaves, the usual sheaf condition is equivalent to the unique gluing formulation.
Русский
Для прешейфов значений в типах условие шейфов эквивалентно формулировке уникальной слепки.
LaTeX
$$$$\text{IsSheaf } F \iff \text{IsSheafUniqueGluing } F,$$$$
Lean4
/-- For type-valued presheaves, the sheaf condition in terms of unique gluings is equivalent to the
usual sheaf condition.
-/
theorem isSheaf_iff_isSheafUniqueGluing_types : F.IsSheaf ↔ F.IsSheafUniqueGluing :=
by
simp_rw [isSheaf_iff_isSheafPairwiseIntersections, IsSheafPairwiseIntersections, Types.isLimit_iff,
IsSheafUniqueGluing, isGluing_iff_pairwise]
refine forall₂_congr fun ι U ↦ ⟨fun h sf cpt ↦ ?_, fun h s hs ↦ ?_⟩
· exact h _ cpt.sectionPairwise.prop
· specialize
h (fun i ↦ s <| op <| Pairwise.single i) fun i j ↦
(hs <| op <| Pairwise.Hom.left i j).trans (hs <| op <| Pairwise.Hom.right i j).symm
convert h; ext (i | ⟨i, j⟩)
· rfl
· exact (hs <| op <| Pairwise.Hom.left i j).symm
