instCofibrationInlOfIsStableUnderCobaseChangeCofibrations

English

If the class of cofibrations is stable under cobase change and g is a cofibration, then the left pushout leg in f-g is a cofibration.

Русский

Если кофибрации замкнуты под cobase change и g — кофибрация, то левая стрелка в пушауте также кофибрация.

LaTeX

$$$[\\text{IsStableUnderCobaseChange}(\\mathrm{cofibrations}(C))]\\,[}\\text{HasPushout }f g] \\Rightarrow \\mathrm{Cofibration}(\\mathrm{pushout}.inl f g).$$$

Lean4

instance [(cofibrations C).IsStableUnderCobaseChange] [hg : Cofibration g] : Cofibration (pushout.inl f g) :=
  by
  rw [cofibration_iff] at hg ⊢
  exact MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g) hg

Похожие утверждения