Theorems · Definition · category theory

CategoryTheory.IsCardinalFiltered.coeq

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [CategoryTheory.IsCardinalFiltered J κ] → {K : Type v'} → {j j' : J} → (K → (j ⟶ j')) → HasCardinalLT K κ → J

Given a family of maps f : K → (j ⟶ j') in a κ-filtered category J, with HasCardinalLT K κ, this is an object of J where these morphisms shall be equalized.

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.IsCardinalFiltered