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.