English
Let C be a category with weak equivalences, cofibrations, and fibrations forming a weak factorization system. For any index set J and any family of morphisms f_i: X_i → Y_i (i ∈ J) that are trivial cofibrations, the induced coproduct map ⨿_{i∈J} f_i: ⨿_{i∈J} X_i → ⨿_{i∈J} Y_i is also a trivial cofibration.
Русский
Пусть C — категория с слабыми эквалентностями, кофибрациями и фибрациями, образующими слабую факторизационную систему. Пусть I индексирует семейство морфизмов f_i: X_i → Y_i. Если каждый f_i является тривиальной кофибрацией, то индуциированная копродуктовая стрелка ⨿_{i∈I} f_i: ⨿_{i∈I} X_i → ⨿_{i∈I} Y_i также является тривиальной кофибрацией.
LaTeX
$$$\\forall (f_i)_{i\\in J},\\ \\left(\\forall i\\in J,\\ f_i \\in \\operatorname{trivialCofibrations}(C)\\right) \\Rightarrow \\left(\\coprod_{i\\in J} f_i : \\coprod_{i\\in J} X_i \\to \\coprod_{i\\in J} Y_i \\in \\operatorname{trivialCofibrations}(C)\\right).$$$
Lean4
instance isStableUnderCoproductsOfShape_trivialCofibrations :
(trivialCofibrations C).IsStableUnderCoproductsOfShape J :=
by
rw [← fibrations_llp]
apply MorphismProperty.llp_isStableUnderCoproductsOfShape
