ind — Mathlib

Lean4
/-- 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`.
-/
def ind (P : MorphismProperty C) : MorphismProperty C := fun X Y f ↦
  ∃ (J : Type w) (_ : SmallCategory J) (_ : IsFiltered J) (D : J ⥤ C) (t : (Functor.const J).obj X ⟶ D) (s :
    D ⟶ (Functor.const J).obj Y) (_ : IsColimit (Cocone.mk _ s)), ∀ j, P (t.app j) ∧ t.app j ≫ s.app j = f
Похожие утверждения