instCofibrationInrOfIsStableUnderCobaseChangeCofibrations

English

If the class of cofibrations is stable under cobase change and f is a cofibration, then the right pushout leg is a cofibration.

Русский

Если кофибрации устойчивы к cobase change и f — кофибрация, то правая стрелка пушаута — кофибрация.

LaTeX

$$$[\\text{IsStableUnderCobaseChange}(\\mathrm{cofibrations}(C))]\\ [hf : \\mathrm{Cofibration}(f)] : \\mathrm{Cofibration}(\\mathrm{pushout}.inr f g).$$$

Lean4

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

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