English
Definition of the bijection between morphisms from freeYoneda J X M to F and M → F.val.obj(op X) for F a Sheaf.
Русский
Определение биекции между морфизмами freeYoneda J X M и F и M → F.val.obj(op X) для F, являющегося Sheaf.
LaTeX
$$$\text{freeYonedaHomEquiv} : (\text{freeYoneda J X M} \to F) \simeq (M \to F.{val}.obj(op X))$$$
Lean4
theorem isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) :=
by
intro F G f g hfg
refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)
rintro _ ⟨⟨X, i⟩, rfl⟩ a
apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
simpa only [← Adjunction.homEquiv_naturality_right_symm] using
hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)
