isCofibrant_iff_of_isInitial — Mathlib

English

In a model category context, if an object A is initial and cofibrations respect isomorphisms, then IsCofibrant X is equivalent to Cofibration i for a morphism i: A → X.

Русский

В контексте модельной категории: если A является начальным и свойство cofibrations уважает изоморфизмы, то IsCofibrant X эквивалентно Cofibration i для отображения i: A → X.

LaTeX

$$$\\text{IsCofibrant }X \\iff \\text{Cofibration } i$$$

Lean4

theorem isCofibrant_iff_of_isInitial [(cofibrations C).RespectsIso] {A X : C} (i : A ⟶ X) (hA : IsInitial A) :
    IsCofibrant X ↔ Cofibration i := by
  simp only [cofibration_iff]
  apply (cofibrations C).arrow_mk_iso_iff
  exact Arrow.isoMk (IsInitial.uniqueUpToIso initialIsInitial hA) (Iso.refl _)

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