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

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

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.

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

class CategoryTheory.MorphismProperty.PreIndSpreads {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : Prop

A property of morphisms P is said to pre-ind-spread if P-morphisms out of filtered colimits descend to a finite level. More precisely, let Dᵢ be a filtered family of objects. Then:

• If f : colim Dᵢ ⟶ T satisfies P, there exists an index j and a pushout square

    Dⱼ ----f'---> T'
    |             |
    |             |
    v             v
  colim Dᵢ --f--> T
  

  such that f' satisfies P.

• exists_isPushout {J : Type w} [SmallCategory J] [IsFiltered J] {D : Functor J C} {c : Limits.Cocone D} : ∀ (x : Limits.IsColimit c) {T : C} (f : c.pt ⟶ T), P f → ∃ (j : J) (T' : C) (f' : D.obj j ⟶ T') (g : T' ⟶ T), IsPushout (c.ι.app j) f' f g ∧ P f'

theorem CategoryTheory.MorphismProperty.exists_isPushout_of_isFiltered {C : Type u} {inst✝ : Category.{v, u} C} {P : MorphismProperty C} [self : P.PreIndSpreads] {J : Type w} [SmallCategory J] [IsFiltered J] {D : Functor J C} {c : Limits.Cocone D} : ∀ (x : Limits.IsColimit c) {T : C} (f : c.pt ⟶ T), P f → ∃ (j : J) (T' : C) (f' : D.obj j ⟶ T') (g : T' ⟶ T), IsPushout (c.ι.app j) f' f g ∧ P f'

Alias of CategoryTheory.MorphismProperty.PreIndSpreads.exists_isPushout.

theorem CategoryTheory.MorphismProperty.IsStableUnderComposition.ind_of_preIndSpreads {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [∀ (X : C), IsFinitelyAccessibleCategory (Under X)] [Limits.HasPushouts C] [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange] [P.PreIndSpreads] (H : P ≤ isFinitelyPresentable C) : P.ind.IsStableUnderComposition

If P ind-spreads and all under categories are finitely accessible, ind P is stable under composition if P is.

theorem CategoryTheory.MorphismProperty.IsMultiplicative.ind_of_preIndSpreads {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [∀ (X : C), IsFinitelyAccessibleCategory (Under X)] [Limits.HasPushouts C] [P.IsMultiplicative] [P.IsStableUnderCobaseChange] [P.PreIndSpreads] (H : P ≤ isFinitelyPresentable C) : P.ind.IsMultiplicative

If P ind-spreads and all under categories are finitely accessible, ind P is multiplicative if P is.