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: IfF : C ⥤ Dpreserves finite limits andChas all finite limits, thenFis flat.preservesFiniteLimits_of_flat: IfF : C ⥤ Dis flat, then it preserves all finite limits.preservesFiniteLimits_iff_flat: IfChas all finite limits, thenFis flat iffFis left_exact.lan_preservesFiniteLimits_of_flat: IfF : C ⥤ Dis a flat functor between small categories, then the functorLan F.opbetween presheaves of sets preserves all finite limits.flat_iff_lan_flat: IfC,Dare small andChas all finite limits, thenFis flat iffLan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)is flat.preservesFiniteLimits_iff_lanPreservesFiniteLimits: IfC,Dare small andChas all finite limits, thenFpreserves finite limits iffLan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)does.
class
CategoryTheory.RepresentablyFlat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D is representably flat if the comma category (X/F) is cofiltered for
each X : D.
- cofiltered (X : D) : IsCofiltered (StructuredArrow X F)
Instances
class
CategoryTheory.RepresentablyCoflat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D is representably coflat if the comma category (F/X) is filtered for
each X : D.
- filtered (X : D) : IsFiltered (CostructuredArrow F X)
Instances
instance
CategoryTheory.RepresentablyFlat.of_isRightAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsRightAdjoint]
:
instance
CategoryTheory.RepresentablyCoflat.of_isLeftAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsLeftAdjoint]
:
instance
CategoryTheory.RepresentablyFlat.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[RepresentablyFlat F]
[RepresentablyFlat G]
:
RepresentablyFlat (F.comp G)
theorem
CategoryTheory.RepresentablyFlat.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[RepresentablyFlat F]
{G : Functor C D}
(α : F ≅ G)
:
Being a representably flat functor is closed under natural isomorphisms.
theorem
CategoryTheory.RepresentablyCoflat.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[RepresentablyCoflat F]
{G : Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.representablyCoflat_op_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
theorem
CategoryTheory.representablyFlat_op_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
instance
CategoryTheory.instRepresentablyCoflatOppositeOpOfRepresentablyFlat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[RepresentablyFlat F]
:
instance
CategoryTheory.instRepresentablyFlatOppositeOpOfRepresentablyCoflat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[RepresentablyCoflat F]
:
instance
CategoryTheory.RepresentablyCoflat.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[RepresentablyCoflat F]
[RepresentablyCoflat G]
:
RepresentablyCoflat (F.comp G)
theorem
CategoryTheory.final_of_representablyFlat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[h : RepresentablyFlat F]
:
F.Final
theorem
CategoryTheory.initial_of_representablyCoflat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[h : RepresentablyCoflat F]
:
F.Initial
theorem
CategoryTheory.flat_of_preservesFiniteLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[Limits.HasFiniteLimits C]
(F : Functor C D)
[Limits.PreservesFiniteLimits F]
:
theorem
CategoryTheory.coflat_of_preservesFiniteColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[Limits.HasFiniteColimits C]
(F : Functor C D)
[Limits.PreservesFiniteColimits F]
:
noncomputable def
CategoryTheory.PreservesFiniteLimitsOfFlat.lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type v₁}
[SmallCategory J]
[FinCategory J]
{K : Functor J C}
(F : Functor C D)
[RepresentablyFlat F]
{c : Limits.Cone K}
(hc : Limits.IsLimit c)
(s : Limits.Cone (K.comp F))
:
(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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type v₁}
[SmallCategory J]
[FinCategory J]
{K : Functor J C}
(F : Functor C D)
[RepresentablyFlat F]
{c : Limits.Cone K}
(hc : Limits.IsLimit c)
(s : Limits.Cone (K.comp F))
(x : J)
:
theorem
CategoryTheory.PreservesFiniteLimitsOfFlat.uniq
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type v₁}
[SmallCategory J]
[FinCategory J]
(F : Functor C D)
[RepresentablyFlat F]
{K : Functor J C}
{c : Limits.Cone K}
(hc : Limits.IsLimit c)
(s : Limits.Cone (K.comp F))
(f₁ f₂ : s.pt ⟶ F.obj c.pt)
(h₁ : ∀ (j : J), CategoryStruct.comp f₁ ((F.mapCone c).π.app j) = s.π.app j)
(h₂ : ∀ (j : J), CategoryStruct.comp f₂ ((F.mapCone c).π.app j) = s.π.app j)
:
theorem
CategoryTheory.preservesFiniteLimits_of_flat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[RepresentablyFlat F]
:
Representably flat functors preserve finite limits.
theorem
CategoryTheory.preservesFiniteColimits_of_coflat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[RepresentablyCoflat F]
:
Representably coflat functors preserve finite colimits.
theorem
CategoryTheory.preservesFiniteLimits_iff_flat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[Limits.HasFiniteLimits C]
(F : Functor C D)
:
If C is finitely complete, then F : C ⥤ D is representably flat iff it preserves
finite limits.
theorem
CategoryTheory.preservesFiniteColimits_iff_coflat
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[Limits.HasFiniteColimits C]
(F : Functor C D)
:
If C is finitely cocomplete, then F : C ⥤ D is representably coflat iff it preserves
finite colmits.
noncomputable def
CategoryTheory.lanEvaluationIsoColim
{C D : Type u₁}
[SmallCategory C]
[SmallCategory D]
(E : Type u₂)
[Category.{u₁, u₂} E]
(F : Functor C D)
(X : D)
[∀ (X : D), Limits.HasColimitsOfShape (CostructuredArrow F X) E]
:
F.lan.comp ((evaluation D E).obj X) ≅ ((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X)).comp 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
instance
CategoryTheory.lan_preservesFiniteLimits_of_flat
{C D : Type u₁}
[SmallCategory C]
[SmallCategory D]
(E : Type u₂)
[Category.{u₁, u₂} E]
[HasForget E]
[Limits.HasLimits E]
[Limits.HasColimits E]
[Limits.ReflectsLimits (forget E)]
[Limits.PreservesFilteredColimits (forget E)]
[Limits.PreservesLimits (forget E)]
(F : Functor C D)
[RepresentablyFlat F]
:
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.
instance
CategoryTheory.lan_flat_of_flat
{C D : Type u₁}
[SmallCategory C]
[SmallCategory D]
(E : Type u₂)
[Category.{u₁, u₂} E]
[HasForget E]
[Limits.HasLimits E]
[Limits.HasColimits E]
[Limits.ReflectsLimits (forget E)]
[Limits.PreservesFilteredColimits (forget E)]
[Limits.PreservesLimits (forget E)]
(F : Functor C D)
[RepresentablyFlat F]
:
instance
CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits
{C D : Type u₁}
[SmallCategory C]
[SmallCategory D]
(E : Type u₂)
[Category.{u₁, u₂} E]
[HasForget E]
[Limits.HasLimits E]
[Limits.HasColimits E]
[Limits.ReflectsLimits (forget E)]
[Limits.PreservesFilteredColimits (forget E)]
[Limits.PreservesLimits (forget E)]
[Limits.HasFiniteLimits C]
(F : Functor C D)
[Limits.PreservesFiniteLimits F]
:
theorem
CategoryTheory.flat_iff_lan_flat
{C D : Type u₁}
[SmallCategory C]
[SmallCategory D]
[Limits.HasFiniteLimits C]
(F : Functor C D)
:
theorem
CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits
{C D : Type u₁}
[SmallCategory C]
[SmallCategory D]
[Limits.HasFiniteLimits C]
(F : Functor C D)
:
If C is finitely complete, then F : C ⥤ D preserves finite limits iff
Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves finite limits.