instFibrationFstOfIsStableUnderBaseChangeFibrations

English

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

Русский

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

LaTeX

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

Lean4

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

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