isCofibrant_of_cofibration — Mathlib

English

If i: X→Y is a Cofibration and X is cofibrant, then Y is cofibrant.

Русский

Если стрелка i: X→Y является кофибрацией, а X кофибрирован, то Y также кофибривент.

LaTeX

$$$[\text{IsStableUnderComposition}](\text{cofibrations})\Rightarrow (IsCofibrant Y) \text{ given } i:X\to Y$$$

Lean4

theorem isCofibrant_of_cofibration [(cofibrations C).IsStableUnderComposition] {X Y : C} (i : X ⟶ Y) [Cofibration i]
    [hX : IsCofibrant X] : IsCofibrant Y := by
  rw [isCofibrant_iff] at hX ⊢
  rw [Subsingleton.elim (initial.to Y) (initial.to X ≫ i)]
  infer_instance

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