instHasCoproductSigmaFstSndOfSigmaObj

English

Let f_i be a family of types and g_i: f(i) → C be a family of objects in C. If each g_i has a coproduct and the coproduct over i exists, then the coproduct over the dependent family p ↦ g_i(p.2) exists; injections arise via the universal property of the coproduct.

Русский

Пусть {f_i} задаёт семейство индексов, и для каждого i дано отображение g_i: f(i) → C; если для каждого i существуют coproducts g_i и существует coproduct по всему бинарному индексу, то существует coproduct зависимого семейства p ↦ g_i(p.2).

LaTeX

$$$\\exists Q\\;\\{\\iota_{i,j}: g(i)(j) \\to Q\\}_{i\\in I,\\; j\\in f(i)}\\quad\\text{таким образом} \\; Q \\cong \\coprod_{i\\in I}\\left(\\coprod_{j\\in f(i)} g(i)(j)\\right).$$$

Lean4

instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasCoproduct (g i)] [HasCoproduct fun i => ∐ g i] :
    HasCoproduct fun p : Σ i, f i => g p.1 p.2 where
  exists_colimit :=
    Nonempty.intro
      { cocone := Cofan.mk (∐ fun i => ∐ g i) (fun X => Sigma.ι (g X.1) X.2 ≫ Sigma.ι (fun i => ∐ g i) X.1)
        isColimit :=
          mkCofanColimit _ (fun s => Sigma.desc fun b => Sigma.desc fun c => s.inj ⟨b, c⟩) (by simp)
            (by intro s (m : (∐ fun i ↦ ∐ g i) ⟶ _) w; aesop_cat (add norm simp Sigma.forall)) }

Похожие утверждения