English
Assume F is CofilteredOrEmpty and surjective on all maps; if s ⊆ F.obj i is nonempty, then for every j, the j-th component of F.toPreimages s is nonempty.
Русский
Пусть F ко-фильтрованный или пустой, и все отображения сюръективны; если s ⊆ F.obj i непусто, тогда для каждого j компонент F.toPreimages s непустая.
LaTeX
$$$[hFn : \forall j, Nonempty (F.obj j)]\ (Fsur : \forall \{i j\}, (F.map f).Surjective)\ (hs : s.Nonempty) (j) \Rightarrow Nonempty ((F.toPreimages s).obj j).$$$
Lean4
theorem toPreimages_nonempty_of_surjective [hFn : ∀ j : J, Nonempty (F.obj j)]
(Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f).Surjective) (hs : s.Nonempty) (j) : Nonempty ((F.toPreimages s).obj j) :=
by
simp only [toPreimages_obj, nonempty_coe_sort, nonempty_iInter, mem_preimage]
obtain h | ⟨⟨ji⟩⟩ := isEmpty_or_nonempty (j ⟶ i)
· exact ⟨(hFn j).some, fun ji => h.elim ji⟩
· obtain ⟨y, ys⟩ := hs
obtain ⟨x, rfl⟩ := Fsur ji y
exact ⟨x, fun ji' => (F.thin_diagram_of_surjective Fsur ji' ji).symm ▸ ys⟩
