Ind and pro-properties

Given a morphism property P, we define a morphism property ind P that is satisfied for f : X ⟶ Y if Y is a filtered colimit of Yᵢ and fᵢ : X ⟶ Yᵢ satisfy P.

We show that ind P inherits stability properties from P.

Main definitions

• CategoryTheory.MorphismProperty.ind: f satisfies ind P if f is a filtered colimit of morphisms in P.

Main results:

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

TODOs:

• Dualise to obtain pro P.
• Show ind P is stable under composition if P spreads out (Christian).

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

Let P be a property of morphisms. P.ind is satisfied for f : X ⟶ Y if there exists a family of natural maps tᵢ : X ⟶ Yᵢ and sᵢ : Yᵢ ⟶ Y indexed by J such that

• J is filtered
• Y ≅ colim Yᵢ via {sᵢ}ᵢ
• tᵢ satisfies P for all i
• f = tᵢ ≫ sᵢ for all i.

See CategoryTheory.MorphismProperty.ind_iff_ind_under_mk for an equivalent characterization in terms of Y as an object of Under X.

Equations

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

theorem CategoryTheory.MorphismProperty.exists_hom_of_isFinitelyPresentable {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] [IsFiltered J] {D : Functor J C} {c : Limits.Cocone D} (hc : Limits.IsColimit c) {X A : C} {p : X ⟶ A} (hp : isFinitelyPresentable C p) (s : (Functor.const J).obj X ⟶ D) (f : A ⟶ c.pt) (h : ∀ (j : J), CategoryStruct.comp (s.app j) (c.ι.app j) = CategoryStruct.comp p f) : ∃ (j : J) (q : A ⟶ D.obj j), CategoryStruct.comp p q = s.app j ∧ CategoryStruct.comp q (c.ι.app j) = f

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

theorem CategoryTheory.MorphismProperty.ind_iff_ind_underMk {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {X Y : C} (f : X ⟶ Y) : P.ind f ↔ P.underObj.ind (CategoryTheory.Under.mk f)

theorem CategoryTheory.MorphismProperty.underObj_ind_eq_ind_underObj {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} (X : C) : P.ind.underObj = P.underObj.ind

instance CategoryTheory.MorphismProperty.instRespectsLeftInd {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} (Q : MorphismProperty C) [P.RespectsLeft Q] : P.ind.RespectsLeft Q

instance CategoryTheory.MorphismProperty.instRespectsIsoInd {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.RespectsIso] : P.ind.RespectsIso

theorem CategoryTheory.MorphismProperty.ind_underObj_pushout {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {X Y : C} (g : X ⟶ Y) [Limits.HasPushouts C] [P.IsStableUnderCobaseChange] {f : Under X} (hf : P.underObj.ind f) : P.underObj.ind ((Under.pushout g).obj f)

instance CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeIndOfHasPushouts {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] [Limits.HasPushouts C] : P.ind.IsStableUnderCobaseChange

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

ind is idempotent if P implies finitely presentable.