Theorems · Definition · category theory

CategoryTheory.MorphismProperty.ind

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Ind

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category