Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.ind_iff_exists

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

Defined in

Mathlib.CategoryTheory.MorphismProperty.Ind

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsFinitelyAccessibleCategory