Compactness of the embedded objects of the ind-completion

Objects of a small category C are compact in Ind C: the hom functor out of an embedded object preserves filtered colimits. This is the finite-stage engine of Deligne 2.8 — a morphism from an embedded object into a filtered colimit factors through a stage, and two stage factorisations that agree in the colimit are merged by transition maps of the diagram.

• RS.indOf — the canonical embedding C ⥤ Ind C (Mathlib's Ind.yoneda, re-exported);
• RS.indOfCoyonedaIso — mapping out of indOf.obj X in Ind C is mapping out of the representable yoneda.obj X after applying the inclusion Ind C ⥤ Cᵒᵖ ⥤ Type v;
• RS.preservesColimitsOfShape_coyoneda_indOf and the derived PreservesFilteredColimits instance — compactness itself;
• RS.exists_factor_of_hom_colimit — factorisation through a stage;
• RS.factor_eq_of_hom_colimit — merging of stage factorisations;
• RS.comp_ι_eq_comp_ι_iff — equality after passing to the colimit is equality at some later stage.

The route: the inclusion Ind C ⥤ Cᵒᵖ ⥤ Type v is fully faithful and creates (hence preserves) filtered colimits, and mapping out of a representable presheaf preserves all colimits that exist (Mathlib's Limits.Preserves.Yoneda); the stage lemmas then read off elements of a filtered colimit of types (Types.jointly_surjective', Types.FilteredColimit.colimit_eq_iff).

@[reducible, inline]

noncomputable abbrev RS.indOf {C : Type v} [CategoryTheory.SmallCategory C] : CategoryTheory.Functor C (CategoryTheory.Ind C)

The canonical embedding of a small category into its ind-completion: Mathlib's Ind.yoneda, re-exported under the name used throughout the Deligne development.

Equations

• RS.indOf = CategoryTheory.Ind.yoneda

noncomputable def RS.indOfCoyonedaIso {C : Type v} [CategoryTheory.SmallCategory C] (X : C) : CategoryTheory.coyoneda.obj (Opposite.op (indOf.obj X)) ≅ (CategoryTheory.Ind.inclusion C).comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.yoneda.obj X)))

Mapping out of an embedded object of Ind C is mapping out of its representable presheaf: the inclusion Ind C ⥤ Cᵒᵖ ⥤ Type v is fully faithful and carries indOf.obj X to an object isomorphic to yoneda.obj X.

Equations

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

instance RS.preservesColimitsOfShape_coyoneda_indOf {C : Type v} [CategoryTheory.SmallCategory C] (X : C) (I : Type v) [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : CategoryTheory.Limits.PreservesColimitsOfShape I (CategoryTheory.coyoneda.obj (Opposite.op (indOf.obj X)))

Objects of C are compact in Ind C: the hom functor out of an embedded object preserves filtered colimits of any given small shape.

instance RS.preservesFilteredColimits_coyoneda_indOf {C : Type v} [CategoryTheory.SmallCategory C] (X : C) : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.coyoneda.obj (Opposite.op (indOf.obj X)))

Compactness, packaged: the hom functor out of an embedded object preserves all (small) filtered colimits.

theorem RS.ι_comp_coyoneda_indOf {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (X : C) (i : I) (g : indOf.obj X ⟶ D.obj i) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι (D.comp (CategoryTheory.coyoneda.obj (Opposite.op (indOf.obj X)))) i)) g = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.preservesColimitIso (CategoryTheory.coyoneda.obj (Opposite.op (indOf.obj X))) D).hom) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.colimit.ι D i))

Stage description of an element of the hom-out-of-indOf functor applied to a filtered colimit: the colimit injection of the diagram of hom sets is postcomposition with the colimit injection of the diagram, read through the preservation isomorphism.

theorem RS.exists_factor_of_hom_colimit {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (X : C) (f : indOf.obj X ⟶ CategoryTheory.Limits.colimit D) : ∃ (i : I) (g : indOf.obj X ⟶ D.obj i), CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.colimit.ι D i) = f

Factorisation through a stage (half of Kashiwara–Schapira 6.1.19, the surjectivity half of the compactness formula): a morphism from an embedded object into a filtered colimit in Ind C factors through one of the stages of the diagram.

theorem RS.factor_eq_of_hom_colimit {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (X : C) {i j : I} (g₁ : indOf.obj X ⟶ D.obj i) (g₂ : indOf.obj X ⟶ D.obj j) (h : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.colimit.ι D i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.colimit.ι D j)) : ∃ (k : I) (α : i ⟶ k) (β : j ⟶ k), CategoryTheory.CategoryStruct.comp g₁ (D.map α) = CategoryTheory.CategoryStruct.comp g₂ (D.map β)

Merging of stage factorisations (the injectivity half of the compactness formula): two stage factorisations that agree after passing to the filtered colimit are merged by transition maps of the diagram.

theorem RS.comp_ι_eq_comp_ι_iff {C : Type v} [CategoryTheory.SmallCategory C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (X : C) {i : I} (g₁ g₂ : indOf.obj X ⟶ D.obj i) : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.colimit.ι D i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.colimit.ι D i) ↔ ∃ (k : I) (α : i ⟶ k), CategoryTheory.CategoryStruct.comp g₁ (D.map α) = CategoryTheory.CategoryStruct.comp g₂ (D.map α)

Equality in the colimit is equality at a stage: two parallel morphisms from an embedded object to a stage of a filtered diagram agree after passing to the colimit iff they agree after some transition map. (In an additive setting, applied with g₂ = 0: a stage morphism vanishes in the colimit iff it vanishes at some later stage.)