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 #

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

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

Equations

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
@[class]
structure category_theory.representably_flat {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
Prop

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