English
For a functor F: C ⥤ D between small categories with finite limits (C has finite limits), F is representably flat if and only if its left Kan extension along op(F), F.op.lan, is representably flat.
Русский
Для функторa F: C ⥤ D между малыми категориями с конечными пределами F представимо плоский тогда и только тогда, когда его левое Кан-подовершение вдоль опре(F) F.op.lan также представимо плоское.
LaTeX
$$$\\operatorname{RepresentablyFlat} F \\;\\iff\\; \\operatorname{RepresentablyFlat}(F^{op}.\\mathrm{lan})$$$
Lean4
theorem flat_iff_lan_flat (F : C ⥤ D) : RepresentablyFlat F ↔ RepresentablyFlat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁) :=
⟨fun _ => inferInstance, fun H =>
by
haveI := preservesFiniteLimits_of_flat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁)
haveI : PreservesFiniteLimits F :=
by
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
intros; apply preservesLimit_of_lan_preservesLimit
apply flat_of_preservesFiniteLimits⟩
