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 [Joh02] 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : 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) : IsCofiltered (StructuredArrow X F)

class CategoryTheory.RepresentablyCoflat {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : 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) : IsFiltered (CostructuredArrow F X)

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

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

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

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

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

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

Being a representably flat functor is closed under natural isomorphisms.

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

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

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

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

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

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

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

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

noncomputable def CategoryTheory.PreservesFiniteLimitsOfFlat.lift {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type v₁} [SmallCategory J] [FinCategory J] {K : Functor J C} (F : Functor C D) [RepresentablyFlat F] {c : Limits.Cone K} (hc : Limits.IsLimit c) (s : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type v₁} [SmallCategory J] [FinCategory J] {K : Functor J C} (F : Functor C D) [RepresentablyFlat F] {c : Limits.Cone K} (hc : Limits.IsLimit c) (s : Limits.Cone (K.comp F)) (x : J) : CategoryStruct.comp (lift F hc s) ((F.mapCone c).π.app x) = s.π.app x

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

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

Representably flat functors preserve finite limits.

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

Representably coflat functors preserve finite colimits.

theorem CategoryTheory.preservesFiniteLimits_iff_flat {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasFiniteLimits C] (F : Functor C D) : RepresentablyFlat F ↔ 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasFiniteColimits C] (F : Functor C D) : RepresentablyCoflat F ↔ 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₁} [SmallCategory C] [SmallCategory D] (E : Type u₂) [Category.{u₁, u₂} E] (F : Functor C D) (X : D) [∀ (X : D), Limits.HasColimitsOfShape (CostructuredArrow F X) E] : F.lan.comp ((evaluation D E).obj X) ≅ ((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X)).comp 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.

instance CategoryTheory.lan_preservesFiniteLimits_of_flat {C D : Type u₁} [SmallCategory C] [SmallCategory D] (E : Type u₂) [Category.{u₁, u₂} E] [HasForget E] [Limits.HasLimits E] [Limits.HasColimits E] [Limits.ReflectsLimits (forget E)] [Limits.PreservesFilteredColimits (forget E)] [Limits.PreservesLimits (forget E)] (F : Functor C D) [RepresentablyFlat F] : 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.

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

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

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

theorem CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits {C D : Type u₁} [SmallCategory C] [SmallCategory D] [Limits.HasFiniteLimits C] (F : Functor C D) : Limits.PreservesFiniteLimits F ↔ 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.