instFibrationSndOfIsFibrant — Mathlib

English

If X is fibrant, then prod.snd : X × Y → Y is a fibration (under suitable base-change assumptions).

Русский

Если X фибривант, то prod.snd: X×Y → Y — фибрация (при подходящих условиях базового изменения).

LaTeX

$$$\text{Fibration}(\mathrm{prod.snd})$$$

Lean4

instance [HasTerminal C] [HasBinaryProduct X Y] [hX : IsFibrant X] : Fibration (prod.snd : X ⨯ Y ⟶ Y) :=
  by
  rw [isFibrant_iff] at hX
  rw [fibration_iff] at hX ⊢
  exact
    MorphismProperty.of_isPullback
      (IsPullback.of_isLimit_binaryFan_of_isTerminal (limit.isLimit (pair X Y)) terminalIsTerminal) hX

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