mathlib3 documentation

category_theory.functor.flat

Representably flat functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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₁} [category_theory.category C] {J : Type w} [category_theory.small_category J] {K : J ⥤ C} (c : category_theory.limits.cone K) (j : J) :

(category_theory.structured_arrow_cone.to_diagram c).obj j = category_theory.structured_arrow.mk (c.π.app j)

@[simp]

theorem category_theory.structured_arrow_cone.to_diagram_map {C : Type u₁} [category_theory.category C] {J : Type w} [category_theory.small_category J] {K : J ⥤ C} (c : category_theory.limits.cone K) (j k : J) (g : j ⟶ k) :

(category_theory.structured_arrow_cone.to_diagram c).map g = category_theory.structured_arrow.hom_mk g _

def category_theory.structured_arrow_cone.to_diagram {C : Type u₁} [category_theory.category C] {J : Type w} [category_theory.small_category J] {K : J ⥤ C} (c : category_theory.limits.cone K) :

J ⥤ category_theory.structured_arrow c.X K

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

category_theory.structured_arrow_cone.to_diagram c = {obj := λ (j : J), category_theory.structured_arrow.mk (c.π.app j), map := λ (j k : J) (g : j ⟶ k), category_theory.structured_arrow.hom_mk g _, map_id' := _, map_comp' := _}

def category_theory.structured_arrow_cone.diagram_to_cone {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.small_category J] (F : C ⥤ D) {X : D} (G : J ⥤ category_theory.structured_arrow X F) :

category_theory.limits.cone (G ⋙ category_theory.structured_arrow.proj X F ⋙ F)

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

Equations

category_theory.structured_arrow_cone.diagram_to_cone F G = {X := X, π := {app := λ (j : J), (G.obj j).hom, naturality' := _}}

@[simp]

theorem category_theory.structured_arrow_cone.diagram_to_cone_X {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.small_category J] (F : C ⥤ D) {X : D} (G : J ⥤ category_theory.structured_arrow X F) :

(category_theory.structured_arrow_cone.diagram_to_cone F G).X = X

@[simp]

theorem category_theory.structured_arrow_cone.diagram_to_cone_π_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.small_category J] (F : C ⥤ D) {X : D} (G : J ⥤ category_theory.structured_arrow X F) (j : J) :

(category_theory.structured_arrow_cone.diagram_to_cone F G).π.app j = (G.obj j).hom

@[simp]

theorem category_theory.structured_arrow_cone.to_cone_X {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.small_category J] {K : J ⥤ C} (F : C ⥤ D) (c : category_theory.limits.cone K) {X : D} (f : X ⟶ F.obj c.X) :

(category_theory.structured_arrow_cone.to_cone F c f).X = category_theory.structured_arrow.mk f

def category_theory.structured_arrow_cone.to_cone {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.small_category J] {K : J ⥤ C} (F : C ⥤ D) (c : category_theory.limits.cone K) {X : D} (f : X ⟶ F.obj c.X) :

category_theory.limits.cone (category_theory.structured_arrow_cone.to_diagram (F.map_cone c) ⋙ category_theory.structured_arrow.map f ⋙ category_theory.structured_arrow.pre X K F)

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

category_theory.structured_arrow_cone.to_cone F c f = {X := category_theory.structured_arrow.mk f, π := {app := λ (j : J), category_theory.structured_arrow.hom_mk (c.π.app j) _, naturality' := _}}

@[simp]

theorem category_theory.structured_arrow_cone.to_cone_π_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.small_category J] {K : J ⥤ C} (F : C ⥤ D) (c : category_theory.limits.cone K) {X : D} (f : X ⟶ F.obj c.X) (j : J) :

(category_theory.structured_arrow_cone.to_cone F c f).π.app j = category_theory.structured_arrow.hom_mk (c.π.app j) _

@[class]

structure category_theory.representably_flat {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

Prop

cofiltered : ∀ (X : D), category_theory.is_cofiltered (category_theory.structured_arrow X F)

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

Instances of this typeclass

@[protected, instance]

def category_theory.representably_flat.id {C : Type u₁} [category_theory.category C] :

category_theory.representably_flat (𝟭 C)

@[protected, instance]

def category_theory.representably_flat.comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.representably_flat F] [category_theory.representably_flat G] :

category_theory.representably_flat (F ⋙ G)

theorem category_theory.cofiltered_of_has_finite_limits {C : Type u₁} [category_theory.category C] [category_theory.limits.has_finite_limits C] :

category_theory.is_cofiltered C

theorem category_theory.flat_of_preserves_finite_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_finite_limits C] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] :

category_theory.representably_flat F

noncomputable def category_theory.preserves_finite_limits_of_flat.lift {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v₁} [category_theory.small_category J] [category_theory.fin_category J] {K : J ⥤ C} (F : C ⥤ D) [category_theory.representably_flat F] {c : category_theory.limits.cone K} (hc : category_theory.limits.is_limit c) (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

category_theory.preserves_finite_limits_of_flat.lift F hc s = let s' : category_theory.limits.cone (category_theory.structured_arrow_cone.to_diagram s ⋙ category_theory.structured_arrow.pre s.X K F) := category_theory.is_cofiltered.cone (category_theory.structured_arrow_cone.to_diagram s ⋙ category_theory.structured_arrow.pre s.X K F) in s'.X.hom ≫ F.map (hc.lift ((category_theory.limits.cones.postcompose {app := λ (X : J), 𝟙 (((category_theory.structured_arrow_cone.to_diagram s ⋙ category_theory.structured_arrow.pre s.X K F) ⋙ category_theory.structured_arrow.proj s.X F).obj X), naturality' := _}).obj ((category_theory.structured_arrow.proj s.X F).map_cone s')))

theorem category_theory.preserves_finite_limits_of_flat.fac {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v₁} [category_theory.small_category J] [category_theory.fin_category J] {K : J ⥤ C} (F : C ⥤ D) [category_theory.representably_flat F] {c : category_theory.limits.cone K} (hc : category_theory.limits.is_limit c) (s : category_theory.limits.cone (K ⋙ F)) (x : J) :

category_theory.preserves_finite_limits_of_flat.lift F hc s ≫ (F.map_cone c).π.app x = s.π.app x

theorem category_theory.preserves_finite_limits_of_flat.uniq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v₁} [category_theory.small_category J] [category_theory.fin_category J] (F : C ⥤ D) [category_theory.representably_flat F] {K : J ⥤ C} {c : category_theory.limits.cone K} (hc : category_theory.limits.is_limit 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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.representably_flat F] :

category_theory.limits.preserves_finite_limits F

Representably flat functors preserve finite limits.

Equations

category_theory.preserves_finite_limits_of_flat F = category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size F (λ (J : Type v₁) (𝒥 : category_theory.small_category J) (hJ : category_theory.fin_category J), {preserves_limit := id (λ (K : J ⥤ C), {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), {lift := category_theory.preserves_finite_limits_of_flat.lift F hc, fac' := _, uniq' := _}})})

noncomputable def category_theory.preserves_finite_limits_iff_flat {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_finite_limits C] (F : C ⥤ D) :

category_theory.representably_flat F ≃ category_theory.limits.preserves_finite_limits F

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

Equations

category_theory.preserves_finite_limits_iff_flat F = {to_fun := λ (_x : category_theory.representably_flat F), category_theory.preserves_finite_limits_of_flat F, inv_fun := _, left_inv := _, right_inv := _}

noncomputable def category_theory.Lan_evaluation_iso_colim {C D : Type u₁} [category_theory.small_category C] [category_theory.small_category D] (E : Type u₂) [category_theory.category E] (F : C ⥤ D) (X : D) [∀ (X : D), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow F X) E] :

category_theory.Lan F ⋙ (category_theory.evaluation D E).obj X ≅ (category_theory.whiskering_left (category_theory.costructured_arrow F X) C E).obj (category_theory.costructured_arrow.proj F X) ⋙ category_theory.limits.colim

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

Equations

category_theory.Lan_evaluation_iso_colim E F X = category_theory.nat_iso.of_components (λ (G : C ⥤ E), category_theory.limits.colim.map_iso (category_theory.iso.refl (category_theory.Lan.diagram F G X))) _

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

category_theory.Lan_preserves_finite_limits_of_flat E F = category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size (category_theory.Lan F.op) (λ (J : Type u₁) (𝒥 : category_theory.small_category J) (hJ : category_theory.fin_category J), category_theory.limits.preserves_limits_of_shape_of_evaluation (category_theory.Lan F.op) J (λ (K : Dᵒᵖ), category_theory.limits.preserves_limits_of_shape_of_nat_iso (category_theory.Lan_evaluation_iso_colim E F.op K).symm))

@[protected, instance]

@[protected, instance]

Equations

category_theory.Lan_preserves_finite_limits_of_preserves_finite_limits E F = category_theory.Lan_preserves_finite_limits_of_flat E F

theorem category_theory.flat_iff_Lan_flat {C D : Type u₁} [category_theory.small_category C] [category_theory.small_category D] [category_theory.limits.has_finite_limits C] (F : C ⥤ D) :

category_theory.representably_flat F ↔ category_theory.representably_flat (category_theory.Lan F.op)

noncomputable def category_theory.preserves_finite_limits_iff_Lan_preserves_finite_limits {C D : Type u₁} [category_theory.small_category C] [category_theory.small_category D] [category_theory.limits.has_finite_limits C] (F : C ⥤ D) :

category_theory.limits.preserves_finite_limits F ≃ category_theory.limits.preserves_finite_limits (category_theory.Lan F.op)

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

Equations

category_theory.preserves_finite_limits_iff_Lan_preserves_finite_limits F = {to_fun := λ (_x : category_theory.limits.preserves_finite_limits F), infer_instance, inv_fun := λ (_x : category_theory.limits.preserves_finite_limits (category_theory.Lan F.op)), category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size F (λ (J : Type u₁) (𝒥 : category_theory.small_category J) (hJ : category_theory.fin_category J), category_theory.preserves_limit_of_Lan_preserves_limit F J), left_inv := _, right_inv := _}