English
Let R be a presieve on X and P a presheaf of types. Then P is a sheaf for R if and only if the canonical fork built from w P R is a limit (i.e. the fork is an equalizer).
Русский
Пусть R — предшторка над X, P — предобразопределение значений. Тогда P является sheaf для R тогда и только тогда, когда каноническая вилка, построенная из w P R, является предельной (то есть вилочная диаграмма является равноправным пределом).
LaTeX
$$$\text{Presieve.IsSheafFor } P \; R \quad\Longleftrightarrow\quad \exists \!\mathcal{L},\; \text{IsLimit}(\text{Fork.ofι}(_)(w\,P\,R))$$$
Lean4
/-- `P` is a sheaf for `R`, iff the fork given by `w` is an equalizer. -/
@[stacks 00VM]
theorem sheaf_condition : R.IsSheafFor P ↔ Nonempty (IsLimit (Fork.ofι _ (w P R))) :=
by
rw [Types.type_equalizer_iff_unique, ← Equiv.forall_congr_right (firstObjEqFamily P R).toEquiv.symm]
simp_rw [← compatible_iff, ← Iso.toEquiv_fun, Equiv.apply_symm_apply]
apply forall₂_congr
intro x _
apply existsUnique_congr
intro t
rw [Equiv.eq_symm_apply]
constructor
· intro q
funext Y f hf
simpa [forkMap] using q _ _
· intro q Y f hf
rw [← q]
simp [forkMap]
