English
Extensionality for the second object in arrows setup: equality determined by all projections Pi.π on z1 and z2.
Русский
Расширение для второго объекта в схеме стрел: равенство определяется по всем проекциям Pi.π на z1 и z2.
LaTeX
$$$\forall ij,\; (Pi.π _ ij) z_1 = (Pi.π _ ij) z_2 \Rightarrow z_1 = z_2$$$
Lean4
/-- `P` is a sheaf for `Presieve.ofArrows X π`, iff the fork given by `w` is an equalizer. -/
@[stacks 00VM]
theorem sheaf_condition :
(Presieve.ofArrows X π).IsSheafFor P ↔ Nonempty (IsLimit (Fork.ofι (forkMap P X π) (w P X π))) :=
by
rw [Types.type_equalizer_iff_unique, isSheafFor_arrows_iff]
simp only [FirstObj]
rw [← Equiv.forall_congr_right ((equivShrink _).trans (Types.Small.productIso _).toEquiv.symm)]
simp_rw [← compatible_iff_of_small, ← Iso.toEquiv_fun, Equiv.trans_apply, Equiv.apply_symm_apply,
Equiv.symm_apply_apply]
apply forall₂_congr
intro x _
apply existsUnique_congr
intro t
rw [Equiv.eq_symm_apply, ← Equiv.symm_apply_eq]
constructor
· intro q
funext i
simpa [forkMap] using q i
· intro q i
rw [← q]
simp [forkMap]
