Theorems · Definition · category theory

CategoryTheory.IsCardinalFiltered.max

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

If S : K → J is a family of objects of cardinality < κ in a κ-filtered category, this is a choice of objects in J which is the target of a map from any of the objects S k.

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.IsCardinalFiltered