Ind and pro-properties

Given an object property P, we define an object property ind P that is satisfied for X if X is a filtered colimit of Xᵢ and Xᵢ satisfies P.

Main definitions

• CategoryTheory.ObjectProperty.ind: X satisfies ind P if X is a filtered colimit of Xᵢ for Xᵢ in P.

Main results

• CategoryTheory.ObjectProperty.ind_ind: If P implies finitely presentable, then P.ind.ind = P.ind.

TODOs:

• Dualise to obtain CategoryTheory.ObjectProperty.pro.

def CategoryTheory.ObjectProperty.ind {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : ObjectProperty C

X satisfies ind P if X is a filtered colimit of Xᵢ for Xᵢ in P.

Equations

• P.ind X = ∃ (J : Type ?u.3) (x : CategoryTheory.SmallCategory J) (_ : CategoryTheory.IsFiltered J) (pres : CategoryTheory.Limits.ColimitPresentation J X), ∀ (i : J), P (pres.diag.obj i)

theorem CategoryTheory.ObjectProperty.le_ind {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P ≤ P.ind

instance CategoryTheory.ObjectProperty.instNonemptyInd {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} [P.Nonempty] : P.ind.Nonempty

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInd {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} : P.ind.IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.ind_ind {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (h : P ≤ isFinitelyPresentable C) [LocallySmall.{w, v, u} C] : P.ind.ind = P.ind

ind is idempotent if P implies finitely presentable.

theorem CategoryTheory.ObjectProperty.of_essentiallySmall_index {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X : C} {J : Type u_1} [Category.{v_1, u_1} J] [EssentiallySmall.{w, v_1, u_1} J] [IsFiltered J] (pres : Limits.ColimitPresentation J X) (h : ∀ (i : J), P (pres.diag.obj i)) : P.ind X

theorem CategoryTheory.ObjectProperty.ind_iff_exists {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (H : P ≤ isFinitelyPresentable C) [IsFinitelyAccessibleCategory C] {X : C} : P.ind X ↔ ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), CategoryStruct.comp u v = g ∧ P W

If C is finitely accessible and P implies finitely presentable, then X satisfies ind P if and only if every morphism Z ⟶ X from a finitely presentable object factors via an object satisfying P.

theorem CategoryTheory.ObjectProperty.ind_inverseImage_le {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : ObjectProperty D) (F : Functor C D) [Limits.PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F] : (P.inverseImage F).ind ≤ P.ind.inverseImage F

theorem CategoryTheory.ObjectProperty.ind_inverseImage_eq_of_isEquivalence {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : ObjectProperty D) (F : Functor C D) [P.IsClosedUnderIsomorphisms] [F.IsEquivalence] : (P.inverseImage F).ind = P.ind.inverseImage F

theorem CategoryTheory.ObjectProperty.ind_iff_of_equivalence {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : ObjectProperty D) (e : C ≌ D) [P.IsClosedUnderIsomorphisms] (X : D) : (P.inverseImage e.functor).ind (e.inverse.obj X) ↔ P.ind X

instance CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_ind_discrete {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {ι : Type u_1} [Small.{w, u_1} ι] [P.IsClosedUnderLimitsOfShape (Discrete ι)] [Limits.HasProductsOfShape ι C] [Limits.IsIPCOfShape.{w, u_1, v, u} ι C] : P.ind.IsClosedUnderLimitsOfShape (Discrete ι)