English
Joyal's trick: cofibrations have the left lifting property with respect to trivial fibrations, derived from left lifting of trivial cofibrations w.r.t fibrations plus consequences of model axioms.
Русский
Трюк Джояля: кофибрикации обладают левой тягой к тривиальным фибрациям, выводится из левой тяги тривиальных кофибрикаций к фибрациям и последствий аксиом модели.
LaTeX
$$$\text{HasLiftingProperty} \; (\text{Cofibration}, \text{TrivialFibration})$ under the given hypotheses$$
Lean4
/-- Joyal's trick: that cofibrations have the left lifting property
with respect to trivial fibrations follows from the left lifting property
of trivial cofibrations with respect to fibrations and a few other
consequences of the model categories axioms. -/
theorem hasLiftingProperty_of_joyalTrick [HasFactorization (cofibrations C) (trivialFibrations C)] [HasPushouts C]
[(cofibrations C).IsStableUnderComposition] [(cofibrations C).IsStableUnderCobaseChange]
(h :
∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p)
{A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [Fibration p] [WeakEquivalence p] : HasLiftingProperty i p
where
sq_hasLift {f g}
sq := by
let h := factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g sq.w)
have sq' : CommSq (𝟙 X) (pushout.inl _ _ ≫ h.i) p h.p := .mk
have h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p) := by simpa
have h₂ := comp_mem _ _ _ ((cofibrations C).of_isPushout (IsPushout.of_hasPushout f i) (mem_cofibrations i)) h.hi
rw [← cofibration_iff] at h₂
have : WeakEquivalence (pushout.inl f i ≫ h.i) :=
by
rw [weakEquivalence_iff] at h₁ ⊢
exact of_postcomp _ _ _ h.hp.2 h₁
exact ⟨⟨{
l := pushout.inr f i ≫ h.i ≫ sq'.lift
fac_left := by simpa only [assoc, comp_id, pushout.condition_assoc] using f ≫= sq'.fac_left }⟩⟩
