English
A presieve P is a sheaf for S if and only if the fork built from the equalizer maps is a limit; equivalently, P satisfies the equalizer condition for the fork built from forkMap and the first/second maps over S.
Русский
Предпосев P является онашной для S тогда и только тогда, когда форк, построенный из равносходящего мода, является пределом; эквивалентно, P удовлетворяет условию равнозначности для форка, построенного из forkMap и первых/вторых отображений над S.
LaTeX
$$$\\text{Presieve.IsSheafFor}(P, S) \\iff \\text{Nonempty}(\\text{IsLimit}(\\text{Fork.ofι} (\\text{Equalizer.forkMap } P S.arrows) \\cdots ))$$$
Lean4
/-- `P` is a sheaf for `S`, iff the fork given by `w` is an equalizer. -/
theorem equalizer_sheaf_condition : Presieve.IsSheafFor P (S : Presieve X) ↔ Nonempty (IsLimit (Fork.ofι _ (w P S))) :=
by
rw [Types.type_equalizer_iff_unique, ← Equiv.forall_congr_right (firstObjEqFamily P (S : Presieve X)).toEquiv.symm]
simp_rw [← compatible_iff]
simp only [inv_hom_id_apply, Iso.toEquiv_symm_fun]
apply forall₂_congr
intro x _
apply existsUnique_congr
intro t
rw [← Iso.toEquiv_symm_fun]
rw [Equiv.eq_symm_apply]
constructor
· intro q
funext Y f hf
simpa [firstObjEqFamily, forkMap] using q _ _
· intro q Y f hf
rw [← q]
simp [firstObjEqFamily, forkMap]
