English
Let h be a family of Ind-objects given by f a ↦ (f a) and assume h holds; then the pointwise product ∏ᶜ yoneda.obj ∘ g is an Ind-object, and more generally, the Pi construction preserves Ind-objects under suitable hypotheses.
Русский
Пусть h задаёт, что для каждого a из α ∈ C, yoneda.obj ∘ g является Ind-объектом; тогда ∏ᶜ f существует как Ind-объект.
LaTeX
$$$\IsIndObject (\prod^{\mathsf{c}} f)$$$
Lean4
theorem isIndObject_pi (h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)) (f : α → Cᵒᵖ ⥤ Type v)
(hf : ∀ a, IsIndObject (f a)) : IsIndObject (∏ᶜ f) :=
by
let F := fun a => (hf a).presentation.F ⋙ yoneda
suffices (∏ᶜ f ≅ colimit (pointwiseProduct F)) from (isIndObject_colimit _ _ (fun i => h _)).map this.inv
refine Pi.mapIso (fun s => ?_) ≪≫ (asIso (colimitPointwiseProductToProductColimit F)).symm
exact IsColimit.coconePointUniqueUpToIso (hf s).presentation.isColimit (colimit.isColimit _)
