Finite-limit-preserving presheaves

In this file we prove that if C is a small finitely cocomplete category and A : Cᵒᵖ ⥤ Type u is a presheaf, then CostructuredArrow yoneda A is filtered (equivalently, the category of elements of A is cofiltered) if and only if A preserves finite limits.

This is one of the keys steps of establishing the equivalence Ind C ≌ (Cᵒᵖ ⥤ₗ Type u) (here, Cᵒᵖ ⥤ₗ Type u is the category of left exact functors) for a small finitely cocomplete category C.

Implementation notes

In the entire file, we are careful about details like functor associativity to ensure that we do not end up in situations where we have morphisms like colimit.ι F i ≫ f, where the domain of f is colimit G where F and G are definitionally equal but not syntactically equal. In these situations, lemmas about colimit.ι G i ≫ f cannot be applied using rw and simp, forcing the use of erw. In particular, for us this means that HasColimit.isoOfNatIso (Iso.refl _) is better than Iso.refl _ and that we should be very particular about functor associativity.

The theorem is also true for large categories and the proof given here generalizes to this case on paper. However, our infrastructure for commuting finite limits of shape J and filtered colimits of shape K is fundamentally not equipped to deal with the case where not all limits of shape K exist. In fact, not even the definition colimitLimitToLimitColimit can be written down if not all limits of shape K exist. Refactoring this to the level of generality we need would be a major undertaking. Since the application to the category of Ind-objects only require the case where C is small, we leave this as a TODO.

References

• [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Proposition 3.3.13
• [F. Borceux, Handbook of Categorical Algebra 1][borceux-vol1], Proposition 6.1.2

theorem CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) [CategoryTheory.Limits.PreservesFiniteLimits A] : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)

If C is a finitely cocomplete category and A : Cᵒᵖ ⥤ Type u is a presheaf that preserves finite limites, then CostructuredArrow yoneda A is filtered.

One direction of Proposition 3.3.13 of [Kashiwara2006].

def CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange {C : Type u} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (Type u))

(Implementation) This is the bifunctor we will apply "filtered colimits commute with finite limits" to.

Equations

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

def CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso {C : Type u} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) : CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K ≅ K.comp (CategoryTheory.coyoneda.comp ((CategoryTheory.whiskeringLeft (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) C (Type u)).obj (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A)))

(Implementation) The definition of functorToInterchange.

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_inv_app_app {C : Type u} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) (X : J) (X✝ : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (a✝ : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).obj X).obj X✝) : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso A K).inv.app X).app X✝ a✝ = a✝

@[simp]

theorem CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_hom_app_app {C : Type u} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) (X : J) (X✝ : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (a✝ : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).obj X).obj X✝) : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso A K).hom.app X).app X✝ a✝ = a✝

def CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange {C : Type u} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) : (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).flip ≅ ((CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A).comp CategoryTheory.yoneda).comp ((CategoryTheory.whiskeringLeft J Cᵒᵖ (Type u)).obj K)

(Implementation) One way to express the flipped version of our functor. We choose this association because the type of Presheaf.tautologicalCocone is Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda), so this association will show up in the proof.

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_hom_app_app {C : Type u} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (X✝ : J) (a✝ : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).flip.obj X).obj X✝) : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange A K).hom.app X).app X✝ a✝ = a✝

@[simp]

theorem CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_inv_app_app {C : Type u} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (X✝ : J) (a✝ : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).flip.obj X).obj X✝) : ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange A K).inv.app X).app X✝ a✝ = a✝

noncomputable def CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) : (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A).comp (CategoryTheory.yoneda.comp ((CategoryTheory.evaluation Cᵒᵖ (Type u)).obj (CategoryTheory.Limits.limit K))) ≅ (CategoryTheory.coyoneda.comp ((CategoryTheory.whiskeringLeft (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) C (Type u)).obj (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A))).obj (CategoryTheory.Limits.limit K)

(Implementation) A natural isomorphism we will need to construct iso.

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) : (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux A K).hom.app = fun (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) => CategoryTheory.CategoryStruct.id (Opposite.unop (CategoryTheory.Limits.limit K) ⟶ X.left)

noncomputable def CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : A.obj (CategoryTheory.Limits.limit K) ≅ CategoryTheory.Limits.limit (K.comp A)

(Implementation) The isomorphism that proves that A preserves finite limits.

Equations

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

theorem CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso A K).hom = CategoryTheory.Limits.limit.post K A

theorem CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.post K A)

theorem CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : CategoryTheory.Limits.PreservesFiniteLimits A

If C is a small finitely cocomplete category and A : Cᵒᵖ ⥤ Type u is a presheaf such that CostructuredArrow yoneda A is filtered, then A preserves finite limits.

One direction of Proposition 3.3.13 of [Kashiwara2006].

theorem CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteLimits A)

If C is a small finitely cocomplete category and A : Cᵒᵖ ⥤ Type u is a presheaf, then CostructuredArrow yoneda A is filtered if and only if A preserves finite limits.

Proposition 3.3.13 of [Kashiwara2006].