English
If W1,W2 form HasFactorization and are closed under retracts, and every W1–W2 square admits a lifting property, then (W1,W2) is a Weak Factorization System with explicitly defined lifting properties.
Русский
Если W1,W2 образуют Factorization с наличием разложения и сохраняются под retracts, и любой квадрат W1–W2 допускает подъем, то (W1,W2) образуют слабую факторизационную систему с явно заданными свойствами подъема.
LaTeX
$$$ \text{HasFactorization}(W_1,W_2) \land W_1\text{IsStableUnderRetracts} \land W_2\text{IsStableUnderRetracts} \land \forall i,p\, (W_1 i \land W_2 p) \Rightarrow HasLiftingProperty i p \Longrightarrow IsWeakFactorizationSystem W_1 W_2.$$
Lean4
theorem mk' [HasFactorization W₁ W₂] [W₁.IsStableUnderRetracts] [W₂.IsStableUnderRetracts]
(h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y), W₁ i → W₂ p → HasLiftingProperty i p) :
IsWeakFactorizationSystem W₁ W₂
where
rlp := rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts (fun _ _ _ hp _ _ _ hi ↦ h _ _ hi hp)
llp := llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts (fun _ _ _ hi _ _ _ hp ↦ h _ _ hi hp)
