instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences

English

If the ambient class of weak equivalences contains identities, then every identity morphism id_X is a weak equivalence.

Русский

Если в классе слабых эквивалентностей содержатся тождественные стрелки, то для любого объекта X стрелка id_X является слабой эквивалентностью.

LaTeX

$$$\forall X\, \mathrm{WeakEquivalence}(\mathrm{id}_X)$$$

Lean4

instance [(weakEquivalences C).ContainsIdentities] (X : C) : WeakEquivalence (𝟙 X) :=
  by
  rw [weakEquivalence_iff]
  apply id_mem

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