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 https://golem.ph.utexas.edu/category/2011/06/flat_functors_and_morphisms_of.html 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

• flat_of_preservesFiniteLimits: If F : C ⥤ D preserves finite limits and C has all finite limits, then F is flat.
• preservesFiniteLimitsOfFlat: If F : C ⥤ D is flat, then it preserves all finite limits.
• preservesFiniteLimitsIffFlat: If C has all finite limits, then F is flat iff F is left_exact.
• lanPreservesFiniteLimitsOfFlat: If F : C ⥤ D is a flat functor between small categories, then the functor Lan F.op between presheaves of sets preserves all finite limits.
• flat_iff_lan_flat: If C, D are small and C has all finite limits, then F is flat iff Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) is flat.
• preservesFiniteLimitsIffLanPreservesFiniteLimits: If C, D are small and C has all finite limits, then F preserves finite limits iff Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) does.

class CategoryTheory.RepresentablyFlat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

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

• cofiltered : ∀ (X : D), CategoryTheory.IsCofiltered (CategoryTheory.StructuredArrow X F)

instance CategoryTheory.RepresentablyFlat.of_isRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsRightAdjoint F] : CategoryTheory.RepresentablyFlat F

Equations

• ⋯ = ⋯

theorem CategoryTheory.RepresentablyFlat.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.RepresentablyFlat (CategoryTheory.Functor.id C)

instance CategoryTheory.RepresentablyFlat.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.RepresentablyFlat F] [CategoryTheory.RepresentablyFlat G] : CategoryTheory.RepresentablyFlat (CategoryTheory.Functor.comp F G)

Equations

• ⋯ = ⋯

theorem CategoryTheory.flat_of_preservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.RepresentablyFlat F

noncomputable def CategoryTheory.PreservesFiniteLimitsOfFlat.lift {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] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K F)) : s.pt ⟶ F.obj c.pt

(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.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.PreservesFiniteLimitsOfFlat.fac {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] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K F)) (x : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesFiniteLimitsOfFlat.lift F hc s) ((F.mapCone c).π.app x) = s.π.app x

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₁ : s.pt ⟶ F.obj c.pt) (f₂ : s.pt ⟶ F.obj c.pt) (h₁ : ∀ (j : J), CategoryTheory.CategoryStruct.comp f₁ ((F.mapCone c).π.app j) = s.π.app j) (h₂ : ∀ (j : J), CategoryTheory.CategoryStruct.comp f₂ ((F.mapCone c).π.app j) = s.π.app j) : f₁ = f₂

noncomputable def CategoryTheory.preservesFiniteLimitsOfFlat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] : CategoryTheory.Limits.PreservesFiniteLimits F

Representably flat functors preserve finite limits.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.preservesFiniteLimitsIffFlat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyFlat F ≃ CategoryTheory.Limits.PreservesFiniteLimits F

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.lanEvaluationIsoColim {C : Type u₁} {D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (E : Type u₂) [CategoryTheory.Category.{u₁, u₂} E] (F : CategoryTheory.Functor C D) (X : D) [∀ (X : D), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.CostructuredArrow F X) E] : CategoryTheory.Functor.comp (CategoryTheory.lan F) ((CategoryTheory.evaluation D E).obj X) ≅ CategoryTheory.Functor.comp ((CategoryTheory.whiskeringLeft (CategoryTheory.CostructuredArrow F X) C E).obj (CategoryTheory.CostructuredArrow.proj F X)) CategoryTheory.Limits.colim

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.lanPreservesFiniteLimitsOfFlat {C : Type u₁} {D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (E : Type u₂) [CategoryTheory.Category.{u₁, u₂} E] [CategoryTheory.ConcreteCategory E] [CategoryTheory.Limits.HasLimits E] [CategoryTheory.Limits.HasColimits E] [CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.lan F.op)

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.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.lan_flat_of_flat {C : Type u₁} {D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (E : Type u₂) [CategoryTheory.Category.{u₁, u₂} E] [CategoryTheory.ConcreteCategory E] [CategoryTheory.Limits.HasLimits E] [CategoryTheory.Limits.HasColimits E] [CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] : CategoryTheory.RepresentablyFlat (CategoryTheory.lan F.op)

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.lanPreservesFiniteLimitsOfPreservesFiniteLimits {C : Type u₁} {D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (E : Type u₂) [CategoryTheory.Category.{u₁, u₂} E] [CategoryTheory.ConcreteCategory E] [CategoryTheory.Limits.HasLimits E] [CategoryTheory.Limits.HasColimits E] [CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.lan F.op)

Equations

• CategoryTheory.lanPreservesFiniteLimitsOfPreservesFiniteLimits E F = inferInstance

theorem CategoryTheory.flat_iff_lan_flat {C : Type u₁} {D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyFlat F ↔ CategoryTheory.RepresentablyFlat (CategoryTheory.lan F.op)

noncomputable def CategoryTheory.preservesFiniteLimitsIffLanPreservesFiniteLimits {C : Type u₁} {D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.PreservesFiniteLimits F ≃ CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.lan F.op)

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

Equations

• One or more equations did not get rendered due to their size.