coproducts_iff — Mathlib

English

For any X, Y in C and morphism f: X → Y, having coproducts for W at f is equivalent to there existing a set J such that W.colimitsOfShape(Discrete J) f holds.

Русский

Для любых X, Y в C и морфизма f: X → Y свойство копродуктов W(f) эквивалентно существованию множества J с W.colimitsOfShape(Discrete J) f.

LaTeX

$$coproducts(W,f) ↔ ∃ J, W.colimitsOfShape(Discrete J) f$$

Lean4

theorem coproducts_iff {X Y : C} (f : X ⟶ Y) : coproducts.{w} W f ↔ ∃ (J : Type w), W.colimitsOfShape (Discrete J) f :=
  by simp only [coproducts, iSup_iff]

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