English
Every Yoneda-presheaf is a sheaf for the coherent topology.
Русский
Каждый предсет Йонеды является шейфом относительно когерентной топологии.
LaTeX
$$$\mathrm{IsSheaf}(\mathrm{coherentTopology}\ C, \mathrm{yoneda.obj} W)$$$
Lean4
/-- Every Yoneda-presheaf is a sheaf for the coherent topology. -/
theorem isSheaf_yoneda_obj (W : C) : Presieve.IsSheaf (coherentTopology C) (yoneda.obj W) :=
by
rw [isSheaf_coherent]
intro X α _ Y π H
have h_colim := isColimitOfEffectiveEpiFamilyStruct Y π H.effectiveEpiFamily.some
rw [← Sieve.generateFamily_eq] at h_colim
intro x hx
let x_ext := Presieve.FamilyOfElements.sieveExtend x
have hx_ext := Presieve.FamilyOfElements.Compatible.sieveExtend hx
let S := Sieve.generate (Presieve.ofArrows Y π)
obtain ⟨t, t_amalg, t_uniq⟩ : ∃! t, x_ext.IsAmalgamation t :=
(Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext
refine ⟨t, ?_, ?_⟩
· convert Presieve.isAmalgamation_restrict (Sieve.le_generate (Presieve.ofArrows Y π)) _ _ t_amalg
exact (Presieve.restrict_extend hx).symm
· exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy
