English
From a factorization data of prod.lift f (id X) into a cofibration followed by a trivial fibration, one obtains a FibrantBrownFactorization f.
Русский
Из данных факторизации prod.lift f (id X) в виде cofibration и тривиальной фибрации получается FibrantBrownFactorization f.
LaTeX
$$$\exists h : MapFactorizationData(\operatorname{trivialCofibrations} C)(\operatorname{fibrations} C)(\mathrm{prod.lift} f (\mathrm{id} X)) \Rightarrow \text{FibrantBrownFactorization } f$$$
Lean4
/-- The term in `CofibrantBrownFactorization f` that is deduced from
a factorization of `prod.lift f (𝟙 X) : X ⟶ Y ⨯ X`
as a cofibration followed by a trivial fibration. -/
@[simps]
noncomputable def mk' [IsFibrant X] [IsFibrant Y]
(h : MapFactorizationData (trivialCofibrations C) (fibrations C) (prod.lift f (𝟙 X))) : FibrantBrownFactorization f
where
Z := h.Z
i := h.i
p := h.p ≫ prod.fst
r := h.p ≫ prod.snd
hi := by rw [mem_trivialCofibrations_iff]; constructor <;> infer_instance
hp := by rw [← fibration_iff]; infer_instance
