isFibrant_iff_of_isTerminal — Mathlib

English

Let p: X→Y with a fibration structure and Y terminal; then IsFibrant X iff Fibration p.

Русский

Пусть p: X→Y с фибрационной структурой и Y является терминальным объектом; тогда IsFibrant X эквивално Fibration p.

LaTeX

$$$\text{IsFibrant}(X) \iff \text{Fibration}(p)$$$

Lean4

theorem isFibrant_iff_of_isTerminal [(fibrations C).RespectsIso] {X Y : C} (p : X ⟶ Y) (hY : IsTerminal Y) :
    IsFibrant X ↔ Fibration p := by
  simp only [fibration_iff]
  symm
  apply (fibrations C).arrow_mk_iso_iff
  exact Arrow.isoMk (Iso.refl _) (IsTerminal.uniqueUpToIso hY terminalIsTerminal)

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