English
Let {f_i} be a family of indexable families in a category, and for each i an object-valued family g_i over f(i). If each g_i has a finite product and the product over i of the g_i exists, then the product of the dependent family p ↦ g_i(p.1)(p.2) exists; the projections are obtained by composing the i-th fiber projection with the projection to g_i.
Русский
Пусть дано семейство g_i, индексируемое i, такое что для каждого i существует произведение ∏_{j∈f(i)} g_i(j), и существует произведение ∏_{i} (∏_{j∈f(i)} g_i(j)). Тогда существует произведение зависимого семейства p ↦ g_i(p.1)(p.2); проекции получаются как композиции проекции на i-е множитель и проекции внутри g_i.
LaTeX
$$$\\exists P\\;\\{\\pi_{i,j}: P \\to g(i)(j)\\}_{i\\in I,\\; j\\in f(i)}\\quad\\text{such that}\\quad P \\cong \\prod_{i\\in I}\\left(\\prod_{j\\in f(i)} g(i)(j)\\right).$$$
Lean4
instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ᶜ g i] :
HasProduct fun p : Σ i, f i => g p.1 p.2 where
exists_limit :=
Nonempty.intro
{ cone := Fan.mk (∏ᶜ fun i => ∏ᶜ g i) (fun X => Pi.π (fun i => ∏ᶜ g i) X.1 ≫ Pi.π (g X.1) X.2)
isLimit :=
mkFanLimit _ (fun s => Pi.lift fun b => Pi.lift fun c => s.proj ⟨b, c⟩) (by simp)
(by intro s (m : _ ⟶ (∏ᶜ fun i ↦ ∏ᶜ g i)) w; aesop (add norm simp Sigma.forall)) }
