# Documentation

Mathlib.CategoryTheory.Functor.Flat

# 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₁} [] {D : Type u₂} [] (F : ) :
• cofiltered : ∀ (X : D),

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

Instances
instance CategoryTheory.RepresentablyFlat.comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
noncomputable def CategoryTheory.PreservesFiniteLimitsOfFlat.lift {C : Type u₁} [] {D : Type u₂} [] {J : Type v₁} {K : } (F : ) {c : } (hc : ) :
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.

Instances For
theorem CategoryTheory.PreservesFiniteLimitsOfFlat.fac {C : Type u₁} [] {D : Type u₂} [] {J : Type v₁} {K : } (F : ) {c : } (hc : ) (x : J) :
CategoryTheory.CategoryStruct.comp () ((F.mapCone c).π.app x) = s.app x
theorem CategoryTheory.PreservesFiniteLimitsOfFlat.uniq {C : Type u₁} [] {D : Type u₂} [] {J : Type v₁} (F : ) {K : } {c : } (hc : ) (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₁} [] {D : Type u₂} [] (F : ) :

Representably flat functors preserve finite limits.

Instances For
noncomputable def CategoryTheory.preservesFiniteLimitsIffFlat {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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

Instances For
noncomputable def CategoryTheory.lanEvaluationIsoColim {C : Type u₁} {D : Type u₁} (E : Type u₂) [] (F : ) (X : D) [] :
CategoryTheory.Functor.comp () (().obj X) CategoryTheory.Functor.comp (().obj ()) CategoryTheory.Limits.colim

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

Instances For

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.

theorem CategoryTheory.flat_iff_lan_flat {C : Type u₁} {D : Type u₁} (F : ) :

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