English
If W1 ⪯ W2.llp and W1 is stable under retracts, then W2.llp = W1 (under suitable HasFactorization hypotheses). In particular, retracts of left lifting properties preserve equality under appropriate assumptions.
Русский
Если W1 ⪯ W2.llp и W1 устойчиво к retracts, то W2.llp = W1 при подходящих предположениях факторизации.
LaTeX
$$$W_1\le W_2.llp\quad\Rightarrow\quad W_2.llp=W_1$ (при необходимых условиях факторизации).$$
Lean4
/-- Assume that
1. `C` has binary products and pullbacks,
2. `D` has pullbacks, binary products and a terminal object, and
3. `F : C ⥤ D` is full and preserves binary products and pullbacks.
For an object `X` in a category `D`, the diagonal morphism `X ⟶ X × X` is relatively representable
with respect to `F` if and only if so is every morphism of the form `F.obj a ⟶ X`.
-/
theorem diag_iff {X : D} [HasPullbacks C] [PreservesLimitsOfShape WalkingCospan F] :
F.relativelyRepresentable (Limits.diag X) ↔ ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g :=
⟨fun h _ g => of_diag h g, fun h => diag_of_map_from_obj h⟩
