English
If h is a MapFactorizationData from coprod.desc f (id Y) to a cofibration followed by a trivial fibration, then the corresponding cofibration maps compose correctly to yield the original map.
Русский
Если h — Data факторизации from coprod.desc f (id Y) к cofibration и тривиальной фибрации, то соответствующая coфibration-композиция восстанавливает исходное отображение.
LaTeX
$$$\exists h : MapFactorizationData(\operatorname{cofibrations} C)(\operatorname{trivialFibrations} C)(\mathrm{coprod.desc} f (\mathrm{id} Y)) \Rightarrow \text{CofibrantBrownFactorization } f$$$
Lean4
/-- The term in `CofibrantBrownFactorization f` that is deduced from
a factorization of `coprod.desc f (𝟙 Y) : X ⨿ Y ⟶ Y`
as a cofibration followed by a trivial fibration. -/
@[simps]
noncomputable def mk' [IsCofibrant X] [IsCofibrant Y]
(h : MapFactorizationData (cofibrations C) (trivialFibrations C) (coprod.desc f (𝟙 Y))) :
CofibrantBrownFactorization f where
Z := h.Z
i := coprod.inl ≫ h.i
p := h.p
s := coprod.inr ≫ h.i
hi := by rw [← cofibration_iff]; infer_instance
hp := by rw [mem_trivialFibrations_iff]; constructor <;> infer_instance
