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

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)

Instances

theorem CategoryTheory.RepresentablyFlat.cofiltered {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : CategoryTheory.RepresentablyFlat F] (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) [F.IsRightAdjoint] :

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

Instances For

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₁ : 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.

Instances For

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.

Instances For

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] :

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.

Instances For

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

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 F.op.lan

Equations

⋯ = ⋯

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 F.op.lan

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

Equations

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

Instances For