Representably flat functors #

We define representably flat functors as functors such that the category of structured arrows over X is cofiltered for each X. This concept is also known as flat functors as in [Elephant] Remark C2.3.7, and this name is suggested by Mike Shulman in to avoid confusion with other notions of flatness.

This definition is equivalent to left exact functors (functors that preserves finite limits) when C has all finite limits.

Main results #

A functor F : C ⥤ D is representably-flat functor if the comma category (X/F) is cofiltered for each X : C.


    (Implementation). Given a limit cone c : cone K and a cone s : cone (K ⋙ F) with F representably flat, s can factor through F.map_cone c.

    Instances For
      theorem CategoryTheory.PreservesFiniteLimitsOfFlat.uniq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {J : Type v₁} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {K : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K F)) (f₁ : F.obj (f₂ : F.obj (h₁ : ∀ (j : J), CategoryTheory.CategoryStruct.comp f₁ ((F.mapCone c).π.app j) = j) (h₂ : ∀ (j : J), CategoryTheory.CategoryStruct.comp f₂ ((F.mapCone c).π.app j) = j) :
      f₁ = f₂

      If C is finitely cocomplete, then F : C ⥤ D is representably flat iff it preserves finite limits.

      Instances For

        (Implementation) The evaluation of Lan F at X is the colimit over the costructured arrows over X.

        Instances For

          If C is finitely complete, then F : C ⥤ D preserves finite limits iff Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves finite limits.

          Instances For