instFibrationSndOfIsStableUnderBaseChangeFibrations

English

If the class of fibrations is stable under base change and f is a fibration, then the second projection in the pullback is a fibration.

Русский

Если фибрации устойчивы к базовым изменениям и f — фибрация, то правая проекция в расходке — фибрация.

LaTeX

$$$[\\text{IsStableUnderBaseChange}(\\mathrm{fibrations}(C))] [\\mathrm{Fibration}(f)] : \\mathrm{Fibration}(\\mathrm{pullback}.snd f g).$$$

Lean4

instance [(fibrations C).IsStableUnderBaseChange] [hf : Fibration f] : Fibration (pullback.snd f g) :=
  by
  rw [fibration_iff] at hf ⊢
  exact MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g) hf

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