preservesFiniteLimits_iff_lan_preservesFiniteLimits

English

If C has finite limits, then a functor F: C ⥤ D preserves finite limits if and only if its left Kan extension Lan F.op preserves finite limits.

Русский

Пусть C имеет конечные пределы. Тогда F: C ⥤ D сохраняет конечные пределы тогда и только тогда, когда Lan F.op сохраняет их.

LaTeX

$$$\\operatorname{HasFiniteLimits} C \\;\\Rightarrow\\; (\\operatorname{PreservesFiniteLimits} F \\iff \\operatorname{PreservesFiniteLimits}(F^{op}.\\mathrm{lan}))$$$

Lean4

/-- If `C` is finitely complete, then `F : C ⥤ D` preserves finite limits iff
`Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves finite limits.
-/
theorem preservesFiniteLimits_iff_lan_preservesFiniteLimits (F : C ⥤ D) :
    PreservesFiniteLimits F ↔ PreservesFiniteLimits (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁) :=
  ⟨fun _ ↦ inferInstance, fun _ ↦
    preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁} _ (fun _ _ _ ↦ preservesLimit_of_lan_preservesLimit _ _)⟩

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