English
Let C be a category and A a category with coproducts. If a family of objects S: I → A is separating, then the corresponding family of free Yoneda presheaves, indexed by pairs (X, i) in C × I and given by X ↦ freeYoneda(X, S(i)), is also separating.
Русский
Пусть C — категория, A — категория с копропредставлениями. Если семейство объектов S: I → A разделяющее, то соответствующее семейство свободных предобработчиков Йонеда, индексируемое парами (X, i) ∈ C × I и задаваемое X ↦ freeYoneda(X, S(i)), также разделяет.
LaTeX
$$$ \operatorname{IsSeparating}(\operatorname{Set.range} S) \Rightarrow \operatorname{IsSeparating}\left(\operatorname{Set.range}\left(\lambda (X,i) \mapsto \operatorname{freeYoneda} X (S i)\right)\right)$$$
Lean4
theorem isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) :=
by
intro F G f g h
ext ⟨X⟩
refine hS _ _ ?_
rintro _ ⟨i, rfl⟩ α
apply freeYonedaHomEquiv.symm.injective
simpa only [freeYonedaHomEquiv_symm_comp] using h _ ⟨⟨X, i⟩, rfl⟩ (freeYonedaHomEquiv.symm α)
