English
Define a subfunctor of F by restricting to preimages of a fixed subset s ⊆ F.obj i; the j-th component is the intersection of preimages of s along all arrows j ⟶ i, and maps are restrictions of F.map along those arrows.
Русский
Определим подфунктор toPreimages s ⊆ F, ограничивая к предобразам фиксированного подмножества s ⊆ F.obj i; компоненту по j задаём пересечение по всем стрелкам j ⟶ i предобразов s, а отображения — это ограничения F.map вдоль соответствующих стрелок.
LaTeX
$$$\text{toPreimages } s : J ⥤ Type v$ with$$(\text{obj } j) = \bigcap_{f : j \to i} F.map f^{-1}(s),\quad \text{map } g = \text{restriction}_{F.map g}^{\bigcap_f F.map f^{-1}(s)}.$$$$
Lean4
theorem toPreimages (h : F.IsMittagLeffler) : (F.toPreimages s).IsMittagLeffler :=
(isMittagLeffler_iff_subset_range_comp _).2 fun j =>
by
obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j
obtain ⟨j₂, f₂, h₂⟩ := F.isMittagLeffler_iff_eventualRange.1 h j₁
refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩
rintro _ ⟨⟨x, hx⟩, rfl⟩
have : F.map f₂ x ∈ F.eventualRange j₁ := by
rw [h₂]
exact ⟨_, rfl⟩
obtain ⟨y, hy, h₃⟩ := h.subset_image_eventualRange F (f₃ ≫ f₂) this
refine ⟨⟨y, mem_iInter.2 fun g₂ => ?_⟩, Subtype.ext ?_⟩
· obtain ⟨j₄, f₄, h₄⟩ := IsCofilteredOrEmpty.cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁)
obtain ⟨y, rfl⟩ := F.mem_eventualRange_iff.1 hy f₄
rw [← map_comp_apply] at h₃
rw [mem_preimage, ← map_comp_apply, h₄, ← Category.assoc, map_comp_apply, h₃, ← map_comp_apply]
apply mem_iInter.1 hx
· simp_rw [toPreimages_map, MapsTo.val_restrict_apply]
rw [← Category.assoc, map_comp_apply, h₃, map_comp_apply]
