English
If for a diagram F: J ⥤ Cᵒᵖ ⥤ Type v all objects F.obj i are Ind objects, then the colimit of F is an Ind object.
Русский
Если для диаграммы F: J ⥤ Cᵒᵖ ⥤ Type все F.obj i являются Ind-объектами, то ко-лимит F является Ind-объектом.
LaTeX
$$$\\forall i, \\mathrm{IsIndObject}(F.obj i) \\Rightarrow \\mathrm{IsIndObject}(\\operatorname{colimit} F)$$$
Lean4
theorem isIndObject_colimit (I : Type v) [SmallCategory I] [IsFiltered I] (F : I ⥤ Cᵒᵖ ⥤ Type v)
(hF : ∀ i, IsIndObject (F.obj i)) : IsIndObject (colimit F) :=
by
have : IsFiltered (CostructuredArrow yoneda (colimit F)) := IndizationClosedUnderFilteredColimitsAux.isFiltered F hF
refine
(isIndObject_iff _).mpr
⟨this, ?_⟩
-- It remains to show that `CostructuredArrow yoneda (colimit F)` is finally small. Because we
-- have already shown it is filtered, it suffices to exhibit a small weakly terminal set. For this
-- we use that all the `CostructuredArrow yoneda (F.obj i)` have small weakly terminal sets.
have : ∀ i, ∃ (s : Set (CostructuredArrow yoneda (F.obj i))) (_ : Small.{v} s), ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j) :=
fun i => (hF i).finallySmall.exists_small_weakly_terminal_set
choose s hs j hjs hj using this
refine finallySmall_of_small_weakly_terminal_set (⋃ i, (map (colimit.ι F i)).obj '' (s i)) (fun A => ?_)
obtain ⟨i, y, hy⟩ := FunctorToTypes.jointly_surjective'.{v, v} F _ (yonedaEquiv A.hom)
let y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
obtain ⟨x⟩ := hj _ y'
refine ⟨(map (colimit.ι F i)).obj (j i y'), ?_, ⟨?_⟩⟩
· simp only [Set.mem_iUnion, Set.mem_image]
exact ⟨i, j i y', hjs _ _, rfl⟩
· refine ?_ ≫ (map (colimit.ι F i)).map x
refine homMk (𝟙 A.left) (yonedaEquiv.injective ?_)
simp [-EmbeddingLike.apply_eq_iff_eq, hy, yonedaEquiv_comp, y']
