Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.IsStableUnderComposition.ind_of_preIndSpreads

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [∀ (X : C), CategoryTheory.IsFinitelyAccessibleCategory (CategoryTheory.Under X)]
  [CategoryTheory.Limits.HasPushouts C] [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange] [P.PreIndSpreads],
  P ≤ CategoryTheory.MorphismProperty.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.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Ind

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsFinitelyAccessibleCategoryCategoryTheory.Limits.HasPushoutsCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderCobaseChangeCategoryTheory.MorphismProperty.PreIndSpreads