English
If W1 has a factorization through W2 and W1.IsStableUnderRetracts, and W1 ≤ W2.llp, then W2.llp = W1. Intuitively, LLPs coincide when one already dominates the other under retracts.
Русский
Если W1 имеет факторизацию через W2 и W1 стабилен под retracts, и W1 ≤ W2.llp, то W2.llp = W1. Интуитивно: LLP совпадают, когда один уже доминирует над другим в условиях retracts.
LaTeX
$$$[HasFactorization\ W_1 W_2] \land [W_1.IsStableUnderRetracts] \land (W_1 \le W_2.llp) \Rightarrow W_2.llp = W_1$$$
Lean4
theorem llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts [HasFactorization W₁ W₂]
[W₁.IsStableUnderRetracts] (h₁ : W₁ ≤ W₂.llp) : W₂.llp = W₁ :=
le_antisymm
(fun A B i hi ↦ by
have h := factorizationData W₁ W₂ i
have := hi _ h.hp
simpa using of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi)
h₁
