English
If F is representably flat, then the Lan construction F.op.lan preserves finite limits in E.
Русский
Если FRepresentablyFlat, то Lan F.op.lan сохраняет конечные пределы в E.
LaTeX
$$PreservesFiniteLimits (F.op.lan)$$
Lean4
/-- If `F : C ⥤ D` is a representably flat functor between small categories, then the functor
`Lan F.op` that takes presheaves over `C` to presheaves over `D` preserves finite limits.
-/
noncomputable instance lan_preservesFiniteLimits_of_flat (F : C ⥤ D) [RepresentablyFlat F] :
PreservesFiniteLimits (F.op.lan : _ ⥤ Dᵒᵖ ⥤ E) :=
by
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
intro J _ _
apply preservesLimitsOfShape_of_evaluation (F.op.lan : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J
intro K
haveI : IsFiltered (CostructuredArrow F.op K) := IsFiltered.of_equivalence (structuredArrowOpEquivalence F (unop K))
exact preservesLimitsOfShape_of_natIso (lanEvaluationIsoColim _ _ _).symm
