instSigmaObj — Mathlib

English

If β is a type and g: β → C is a diagram with HasCoproduct g, and every g(b) is projective, then the coproduct ∐ g is projective.

Русский

Если β — множество, g: β → C задаёт копродукт, и каждый g(b) проективен, то копродукт ∐ g проективен.

LaTeX

$$$ \\forall b:\\, β, \\; \\text{Projective}(g(b)) \\Rightarrow \\text{Projective}(\\Sigma g) $$$

Lean4

instance {β : Type v} (g : β → C) [HasCoproduct g] [∀ b, Projective (g b)] : Projective (∐ g) where
  factors f e epi := ⟨Sigma.desc fun b => factorThru (Sigma.ι g b ≫ f) e, by cat_disch⟩

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