English
If W is stable under coproducts, then W.coproducts equals W.
Русский
Если W стабилен по копродуктам, то coproducts(W) = W.
LaTeX
$$W.IsStableUnderCoproducts ? (coproducts(W) = W)$$
Lean4
theorem mk (J : Type*) [W.RespectsIso]
(hW :
∀ (X₁ X₂ : J → C) [HasCoproduct X₁] [HasCoproduct X₂] (f : ∀ j, X₁ j ⟶ X₂ j) (_ : ∀ (j : J), W (f j)),
W (Limits.Sigma.map f)) :
W.IsStableUnderCoproductsOfShape J where
condition X₁ X₂ c₁ c₂ hc₁ hc₂ f hf α
hα := by
let φ := fun j => f.app (Discrete.mk j)
have : HasColimit X₁ := ⟨c₁, hc₁⟩
have : HasColimit X₂ := ⟨c₂, hc₂⟩
have : HasCoproduct fun j ↦ X₁.obj (Discrete.mk j) :=
hasColimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₁.obj j)))
have : HasCoproduct fun j ↦ X₂.obj (Discrete.mk j) :=
hasColimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₂.obj j)))
have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))
refine (W.arrow_mk_iso_iff ?_).1 hf'
refine
Arrow.isoMk ((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)
((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂) ?_
apply colimit.hom_ext
rintro ⟨j⟩
simp [φ, hα]
