English
If W1 ≤ W2.llp and HasFactorization W1 W2, then W2.llp = W1 (lemma variant with left lifting properties).
Русский
Если W1 ⊆ W2.llp и существует факторизация W1 через W2, то W2.llp = W1.
LaTeX
$$$[HasFactorization W_1 W_2] \land (W_1 \le W_2.llp) \Rightarrow W_2.llp = W_1$$$
Lean4
/-- A transfinite composition of shape `J` of morphisms in `W` induces a transfinite
composition of shape `Set.Iic j` (for any `j : J`). -/
noncomputable def iic (j : J) : W.TransfiniteCompositionOfShape (Set.Iic j) (h.F.map (homOfLE bot_le : ⊥ ⟶ j))
where
__ := h.toTransfiniteCompositionOfShape.iic j
map_mem i
hi :=
by
have :=
h.map_mem i.1
(by
rw [not_isMax_iff] at hi ⊢
obtain ⟨i', hi'⟩ := hi
exact ⟨j, lt_of_lt_of_le hi' i'.2⟩)
rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
have eq :
Arrow.mk ((Subtype.mono_coe _).functor.map (homOfLE (Order.le_succ i))) =
Arrow.mk (homOfLE (Order.le_succ i.1)) :=
Arrow.ext rfl (Set.Iic.coe_succ_of_not_isMax hi) rfl
replace eq := congr_arg h.F.mapArrow.obj eq
convert this using 1
