Commit 2021-12-03 16:11 f0a1cd1a

feat(category_theory/*): Representably flat functors (#9519) Defined representably flat functors as functors F : C ⥤ D such that (X/F) is cofiltered for each X : C.

• Proved that if C has all finite limits and F preserves them, then F is flat.
• Proved that flat functors preserves finite limits. In particular, if C is finitely complete, then flat iff left exact.
• Proved that if C, D are small, then F flat implies Lan F.op preserves finite limits implies F preserves finite limits. In particular, if C is finitely cocomplete, then flat iff Lan F.op is left exact.