Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.ind_iff_exists

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P ≤ CategoryTheory.ObjectProperty.isFinitelyPresentable C →
    ∀ [CategoryTheory.IsFinitelyAccessibleCategory C] {X : C},
      P.ind X ↔
        ∀ {Z : C} (g : Z ⟶ X) [CategoryTheory.IsFinitelyPresentable Z],
          ∃ W u v, CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.ObjectProperty.Ind

Cited by

1 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.IsFinitelyAccessibleCategory