instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition

English

Weak equivalences respect isomorphisms: if i is an isomorphism, the property of being a weak equivalence is preserved under isomorphisms, under the stated factorization assumptions.

Русский

Слабые эквивалентности сохраняются под изоморфизмами: если стрелка является изоморфизмом, то свойство слабой эквивалентности сохраняется при изоморфизма, при заданной факторизационной системе.

LaTeX

$$$(\text{weakEquivalences } C).RespectsIso$$$

Lean4

instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] [(weakEquivalences C).IsStableUnderRetracts]
    [(weakEquivalences C).IsStableUnderComposition] : (weakEquivalences C).RespectsIso :=
  MorphismProperty.respectsIso_of_isStableUnderComposition
    (fun _ _ _ (_ : IsIso _) ↦ by
      rw [← weakEquivalence_iff]
      infer_instance)

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