English
Dual form: trivial cofibrations have the left lifting property with respect to fibrations, derived from the left lifting of cofibrations with respect to trivial fibrations and standard model-category consequences.
Русский
Дуальная форма: тривиальные кофибрации имеют левую сверхплотность по отношению к фибрациям, выводится из левой тяги кофибраций по тривиальным фибрациям и стандартных следствий модели.
LaTeX
$$$\text{HasLiftingProperty} \; (\text{TrivialCofibration}, \text{Fibration})$ under the given hypotheses$$
Lean4
/-- Joyal's trick (dual): that trivial cofibrations have the left lifting
property with respect to fibrations follows from the left lifting property
of cofibrations with respect to trivial fibrations and a few other
consequences of the model categories axioms. -/
theorem hasLiftingProperty_of_joyalTrickDual [HasFactorization (trivialCofibrations C) (fibrations C)] [HasPullbacks C]
[(fibrations C).IsStableUnderComposition] [(fibrations C).IsStableUnderBaseChange]
(h :
∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p)
{A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [Fibration p] [WeakEquivalence i] : HasLiftingProperty i p
where
sq_hasLift {f g}
sq := by
let h := factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i sq.w)
have sq' : CommSq h.i i (h.p ≫ pullback.snd _ _) (𝟙 B) := .mk
have h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g) := by simpa
have h₂ := comp_mem _ _ _ h.hp ((fibrations C).of_isPullback (IsPullback.of_hasPullback p g) (mem_fibrations p))
rw [← fibration_iff] at h₂
have : WeakEquivalence (h.p ≫ pullback.snd p g) :=
by
rw [weakEquivalence_iff] at h₁ ⊢
exact of_precomp _ _ _ h.hi.2 h₁
exact ⟨⟨{
l := sq'.lift ≫ h.p ≫ pullback.fst p g
fac_right := by rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right] }⟩⟩
