English
For a sieve S on X, the Yoneda presheaves satisfy the sheaf condition for S for all W in C if and only if S.arrows cocone is a colimit.
Русский
Для сита S на X условие Шейфа для всех Yoneda-преслефов выполняется тогда и только тогда, когда кокон IsColimit S.arrows.cocone.
LaTeX
$$(∀ W, Presieve.IsSheafFor (yoneda.obj W) (S.arrows)) \iff \mathrm{Nonempty}(\mathrm{IsColimit}(S.arrows.cocone))$$
Lean4
/-- The base of a sieve `S` is a colimit of `S` iff all Yoneda-presheaves satisfy
the sheaf condition for `S`.
-/
theorem forallYonedaIsSheaf_iff_colimit (S : Sieve X) :
(∀ W : C, Presieve.IsSheafFor (yoneda.obj W) (S : Presieve X)) ↔ Nonempty (IsColimit S.arrows.cocone) :=
by
constructor
· intro H
refine Nonempty.intro ?_
exact
{ desc := fun s =>
H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s) (yonedaFamily_fromCocone_compatible S s) |>.choose
fac := by
intro s f
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s) (yonedaFamily_fromCocone_compatible S s)
have ht := H.choose_spec.1 f.obj.hom f.property
cat_disch
uniq := by
intro s Fs HFs
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s) (yonedaFamily_fromCocone_compatible S s)
apply H.choose_spec.2 Fs
exact fun _ f hf => HFs ⟨Over.mk f, hf⟩ }
· intro H W x hx
replace H := Classical.choice H
let s := compatibleYonedaFamily_toCocone S.arrows W x hx
use H.desc s
constructor
· exact fun _ f hf => (H.fac s) ⟨Over.mk f, hf⟩
· exact fun g hg => H.uniq s g (fun ⟨⟨f, _, hom⟩, hf⟩ => hg hom hf)
