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_preservesFiniteLimits
: IfF : C ⥤ D
preserves finite limits andC
has all finite limits, thenF
is flat.preservesFiniteLimitsOfFlat
: IfF : C ⥤ D
is flat, then it preserves all finite limits.preservesFiniteLimitsIffFlat
: IfC
has all finite limits, thenF
is flat iffF
is left_exact.lanPreservesFiniteLimitsOfFlat
: IfF : C ⥤ D
is a flat functor between small categories, then the functorLan F.op
between presheaves of sets preserves all finite limits.flat_iff_lan_flat
: IfC
,D
are small andC
has all finite limits, thenF
is flat iffLan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)
is flat.preservesFiniteLimitsIffLanPreservesFiniteLimits
: IfC
,D
are small andC
has all finite limits, thenF
preserves finite limits iffLan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)
does.
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Being a representably flat functor is closed under natural isomorphisms.
(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
Representably flat functors preserve finite limits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
(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
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.
Equations
- ⋯ = ⋯
Equations
- CategoryTheory.lanPreservesFiniteLimitsOfPreservesFiniteLimits E F = inferInstance
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.