has_weakly_initial_of_weakly_initial_set_and_hasProducts

English

If a category has (small) products and a small weakly initial set of objects B: ι → C such that for every A there exists i with a morphism B_i → A, then there exists a weakly initial object T in C; in fact T can be formed as the product of all B_i.

Русский

Если категория имеет (мелкие) произведения и существет малый слабовводный набор B = {B_i}, такой что для каждого A существует i и некоторая морфизм B_i → A, тогда в C существует слабовводный объект; на самом деле T можно взять как произведение всех B_i.

LaTeX

$$$$\exists T\;\forall X\,\exists f: T \to X.$$$$

Lean4

/-- If `C` has (small) products and a small weakly initial set of objects, then it has a weakly initial
object.
-/
theorem has_weakly_initial_of_weakly_initial_set_and_hasProducts [HasProducts.{v} C] {ι : Type v} {B : ι → C}
    (hB : ∀ A : C, ∃ i, Nonempty (B i ⟶ A)) : ∃ T : C, ∀ X, Nonempty (T ⟶ X) :=
  ⟨∏ᶜ B, fun X => ⟨Pi.π _ _ ≫ (hB X).choose_spec.some⟩⟩

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