mathlibdocumentation

category_theory.flat_functors

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_preserves_finite_limits: If F : C ⥤ D preserves finite limits and C has all finite limits, then F is flat.
• preserves_finite_limits_of_flat: If F : C ⥤ D is flat, then it preserves all finite limits.
• preserves_finite_limits_iff_flat: If C has all finite limits, then F is flat iff F is left_exact.
• Lan_preserves_finite_limits_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.
• preserves_finite_limits_iff_Lan_preserves_finite_limits: 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.
@[simp]
theorem category_theory.structured_arrow_cone.to_diagram_obj {C : Type u₁} {J : Type v₁} {K : J C} (j : J) :
@[simp]
theorem category_theory.structured_arrow_cone.to_diagram_map {C : Type u₁} {J : Type v₁} {K : J C} (j k : J) (g : j k) :
def category_theory.structured_arrow_cone.to_diagram {C : Type u₁} {J : Type v₁} {K : J C}  :

Given a cone c : cone K and a map f : X ⟶ c.X, we can construct a cone of structured arrows over X with f as the cone point. This is the underlying diagram.

Equations
def category_theory.structured_arrow_cone.diagram_to_cone {C : Type u₁} {D : Type u₂} {J : Type v₁} (F : C D) {X : D} (G : J ) :

Given a diagram of structured_arrow X Fs, we may obtain a cone with cone point X.

Equations
@[simp]
theorem category_theory.structured_arrow_cone.diagram_to_cone_X {C : Type u₁} {D : Type u₂} {J : Type v₁} (F : C D) {X : D} (G : J ) :
@[simp]
theorem category_theory.structured_arrow_cone.diagram_to_cone_π_app {C : Type u₁} {D : Type u₂} {J : Type v₁} (F : C D) {X : D} (G : J ) (j : J) :
= (G.obj j).hom
@[simp]
theorem category_theory.structured_arrow_cone.to_cone_X {C : Type u₁} {D : Type u₂} {J : Type v₁} {K : J C} (F : C D) {X : D} (f : X F.obj c.X) :
def category_theory.structured_arrow_cone.to_cone {C : Type u₁} {D : Type u₂} {J : Type v₁} {K : J C} (F : C D) {X : D} (f : X F.obj c.X) :

Given a cone c : cone K and a map f : X ⟶ F.obj c.X, we can construct a cone of structured arrows over X with f as the cone point.

Equations
@[simp]
theorem category_theory.structured_arrow_cone.to_cone_π_app {C : Type u₁} {D : Type u₂} {J : Type v₁} {K : J C} (F : C D) {X : D} (f : X F.obj c.X) (j : J) :
@[class]
structure category_theory.representably_flat {C : Type u₁} {D : Type u₂} (F : C D) :
Prop
• 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
@[protected, instance]
def category_theory.representably_flat.id {C : Type u₁}  :
@[protected, instance]
def category_theory.representably_flat.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E)  :
@[protected, instance]
theorem category_theory.flat_of_preserves_finite_limits {C : Type u₁} {D : Type u₂} (F : C D)  :
noncomputable def category_theory.preserves_finite_limits_of_flat.lift {C : Type u₁} {D : Type u₂} {J : Type v₁} {K : J C} (F : C D) (s : category_theory.limits.cone (K F)) :
s.X F.obj c.X

(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
theorem category_theory.preserves_finite_limits_of_flat.fac {C : Type u₁} {D : Type u₂} {J : Type v₁} {K : J C} (F : C D) (s : category_theory.limits.cone (K F)) (x : J) :
(F.map_cone c).π.app x = s.π.app x
theorem category_theory.preserves_finite_limits_of_flat.uniq {C : Type u₁} {D : Type u₂} {J : Type v₁} (F : C D) {K : J C} (s : category_theory.limits.cone (K F)) (f₁ f₂ : s.X F.obj c.X) (h₁ : ∀ (j : J), f₁ (F.map_cone c).π.app j = s.π.app j) (h₂ : ∀ (j : J), f₂ (F.map_cone c).π.app j = s.π.app j) :
f₁ = f₂
noncomputable def category_theory.preserves_finite_limits_of_flat {C : Type u₁} {D : Type u₂} (F : C D)  :

Representably flat functors preserve finite limits.

Equations
noncomputable def category_theory.preserves_finite_limits_iff_flat {C : Type u₁} {D : Type u₂} (F : C D) :

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

Equations
noncomputable def category_theory.Lan_evaluation_iso_colim {C D : Type u₁} (E : Type u₂) (F : C D) (X : D) [∀ (X : D), ] :

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

Equations
@[protected, instance]

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
@[protected, instance]
@[protected, instance]
Equations

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

Equations