hasColimit_of_comp_equivalence — Mathlib

English

HasColimitsOfSize can be transported along an equivalence.

Русский

HasColimitsOfSize можно перенести вдоль эквивалентности.

LaTeX

$$$$ HasColimitsOfSize^{v,u}(C) \\text{ if } E:C\\to D \\text{ is an equivalence and HasColimitsOfSize}^{v,u}(D). $$$$

Lean4

theorem hasColimit_of_comp_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimit (K ⋙ E)] : HasColimit K :=
  by
  rw [hasColimit_iff_of_iso ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)]
  exact hasColimit_comp_equivalence (K ⋙ E) E.inv

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