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.32) (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.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.