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.
• preservesFiniteLimits_of_flat: If F : C ⥤ D is flat, then it preserves all finite limits.
• preservesFiniteLimits_iff_flat: If C has all finite limits, then F is flat iff F is left_exact.
• lan_preservesFiniteLimits_of_flat: 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.
• preservesFiniteLimits_iff_lanPreservesFiniteLimits: 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 if the comma category (X/F) is cofiltered for each X : D.

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

class CategoryTheory.RepresentablyCoflat {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 coflat if the comma category (F/X) is filtered for each X : D.

• filtered : ∀ (X : D), CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow F X)

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) [F.IsRightAdjoint] : CategoryTheory.RepresentablyFlat F

Equations

• ⋯ = ⋯

instance CategoryTheory.RepresentablyCoflat.of_isLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint] : CategoryTheory.RepresentablyCoflat F

Equations

• ⋯ = ⋯

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

theorem CategoryTheory.RepresentablyCoflat.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.RepresentablyCoflat (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 (F.comp G)

Equations

• ⋯ = ⋯

theorem CategoryTheory.RepresentablyFlat.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.RepresentablyFlat F] {G : CategoryTheory.Functor C D} (α : F ≅ G) : CategoryTheory.RepresentablyFlat G

Being a representably flat functor is closed under natural isomorphisms.

theorem CategoryTheory.RepresentablyCoflat.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.RepresentablyCoflat F] {G : CategoryTheory.Functor C D} (α : F ≅ G) : CategoryTheory.RepresentablyCoflat G

theorem CategoryTheory.representablyCoflat_op_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyCoflat F.op ↔ CategoryTheory.RepresentablyFlat F

theorem CategoryTheory.representablyFlat_op_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyFlat F.op ↔ CategoryTheory.RepresentablyCoflat F

instance CategoryTheory.instRepresentablyCoflatOppositeOpOfRepresentablyFlat {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.RepresentablyCoflat F.op

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CategoryTheory.RepresentablyCoflat.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.RepresentablyCoflat F] [CategoryTheory.RepresentablyCoflat G] : CategoryTheory.RepresentablyCoflat (F.comp 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

theorem CategoryTheory.coflat_of_preservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.RepresentablyCoflat 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 (K.comp 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.mapCone 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 (K.comp 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 (K.comp F)) (f₁ 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₂

theorem CategoryTheory.preservesFiniteLimits_of_flat {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.

theorem CategoryTheory.preservesFiniteColimits_of_coflat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyCoflat F] : CategoryTheory.Limits.PreservesFiniteColimits F

Representably coflat functors preserve finite colimits.

theorem CategoryTheory.preservesFiniteLimits_iff_flat {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 complete, then F : C ⥤ D is representably flat iff it preserves finite limits.

theorem CategoryTheory.preservesFiniteColimits_iff_coflat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyCoflat F ↔ CategoryTheory.Limits.PreservesFiniteColimits F

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

noncomputable def CategoryTheory.lanEvaluationIsoColim {C 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] : F.lan.comp ((CategoryTheory.evaluation D E).obj X) ≅ ((CategoryTheory.whiskeringLeft (CategoryTheory.CostructuredArrow F X) C E).obj (CategoryTheory.CostructuredArrow.proj F X)).comp CategoryTheory.Limits.colim

(Implementation) The evaluation of F.lan 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.lan_preservesFiniteLimits_of_flat {C 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 F.op.lan

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

• ⋯ = ⋯

instance CategoryTheory.lan_flat_of_flat {C 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 F.op.lan

Equations

• ⋯ = ⋯

instance CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits {C 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 F.op.lan

Equations

• ⋯ = ⋯

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

theorem CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits {C 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 F.op.lan

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