instCofibrationInrOfIsCofibrant — Mathlib

English

Under the same assumptions as 39487, any iso is a weak equivalence.

Русский

При тех же предположениях, что и в 39487, любой изоморфизм является слабой эквивалентностью.

LaTeX

$$$\forall f,\ \mathrm{IsIso}(f) \Rightarrow \mathrm{WeakEquivalence}(f)$$$

Lean4

instance [HasInitial C] [HasBinaryCoproduct X Y] [hX : IsCofibrant X] : Cofibration (coprod.inr : Y ⟶ X ⨿ Y) :=
  by
  rw [isCofibrant_iff] at hX
  rw [cofibration_iff] at hX ⊢
  exact
    MorphismProperty.of_isPushout
      (IsPushout.of_isColimit_binaryCofan_of_isInitial (colimit.isColimit (pair X Y)) initialIsInitial) hX

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