isEquivalence_preservesColimits — Mathlib

English

If E is an equivalence, then E preserves colimits of all shapes.

Русский

Если E — эквивалентность, то она сохраняет колимиты всех форм.

LaTeX

$$$$\\text{If } E \\text{ isEquivalence, then } E \\text{ preservesColimitsOfSize}. $$$$

Lean4

noncomputable instance (priority := 100) isEquivalence_preservesColimits (E : C ⥤ D) [E.IsEquivalence] :
    PreservesColimitsOfSize.{v, u} E :=
  leftAdjoint_preservesColimits E.adjunction

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