lan_preservesFiniteLimits_of_preservesFiniteLimits

English

Let F: C ⥤ D be a functor between small categories. If F preserves finite limits, then the left Kan extension along Fop, viewed as a functor (F.op.lan), also preserves finite limits.

Русский

Пусть F: C ⥤ D — функция между малыми категориями. Если F сохраняет конечные пределы, то левое Кан-подовершение вдоль F^op, рассматриваемое как F.op.lan, тоже сохраняет конечные пределы.

LaTeX

$$$\\operatorname{PreservesFiniteLimits} F \\Rightarrow \\operatorname{PreservesFiniteLimits}(F^{op}.\\mathrm{lan})$$$

Lean4

instance lan_preservesFiniteLimits_of_preservesFiniteLimits (F : C ⥤ D) [PreservesFiniteLimits F] :
    PreservesFiniteLimits (F.op.lan : _ ⥤ Dᵒᵖ ⥤ E) :=
  by
  haveI := flat_of_preservesFiniteLimits F
  infer_instance

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