hasColimit_of_coreflective — Mathlib

English

If C has colimits and R is coreflective, then D has colimits of shape J.

Русский

Если у C есть колимиты и R является ядром-обращением, то D имеет колимиты формы J.

LaTeX

$$$\\operatorname{HasColimitsOfShape} J C \\Rightarrow (\\text{Coreflective } R \\Rightarrow \\operatorname{HasColimitsOfShape} J D).$$$

Lean4

theorem hasColimit_of_coreflective (F : J ⥤ D) (R : D ⥤ C) [HasColimit (F ⋙ R)] [Coreflective R] : HasColimit F :=
  haveI := comonadicCreatesColimits.{v, u} R
  hasColimit_of_created F R

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