κ-filtered category

If κ is a regular cardinal, we introduce the notion of κ-filtered category J: it means that any functor A ⥤ J from a small category such that Arrow A is of cardinality < κ admits a cocone. This generalizes the notion of filtered category. Indeed, we obtain the equivalence IsCardinalFiltered J ℵ₀ ↔ IsFiltered J. The API is mostly parallel to that of filtered categories.

A preordered type J is a κ-filtered category (i.e. κ-directed set) if any subset of J of cardinality < κ has an upper bound.

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

class CategoryTheory.IsCardinalFiltered (J : Type u) [Category.{v, u} J] (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop

A category J is κ-filtered (for a regular cardinal κ) if any functor F : A ⥤ J from a category A such that HasCardinalLT (Arrow A) κ admits a cocone.

• nonempty_cocone {A : Type w} [SmallCategory A] (F : Functor A J) (hA : HasCardinalLT (Arrow A) κ) : Nonempty (Limits.Cocone F)

theorem CategoryTheory.hasCardinalLT_arrow_walkingParallelFamily {T : Type u} {κ : Cardinal.{w}} (hT : HasCardinalLT T κ) (hκ : Cardinal.aleph0 ≤ κ) : HasCardinalLT (Arrow (Limits.WalkingParallelFamily T)) κ

noncomputable def CategoryTheory.IsCardinalFiltered.cocone {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {A : Type v'} [Category.{u', v'} A] (F : Functor A J) (hA : HasCardinalLT (Arrow A) κ) : Limits.Cocone F

A choice of cocone for a functor F : A ⥤ J such that HasCardinalLT (Arrow A) κ when J is a κ-filtered category, and Arrow A has cardinality < κ.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.IsCardinalFiltered.of_le (J : Type u) [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ' ≤ κ) : IsCardinalFiltered J κ'

theorem CategoryTheory.IsCardinalFiltered.of_equivalence {J : Type u} [Category.{v, u} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {J' : Type u'} [Category.{v', u'} J'] (e : J ≌ J') : IsCardinalFiltered J' κ

noncomputable def CategoryTheory.IsCardinalFiltered.max {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {K : Type u'} (S : K → J) (hS : 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.

Equations

• CategoryTheory.IsCardinalFiltered.max S hS = (CategoryTheory.IsCardinalFiltered.cocone (CategoryTheory.Discrete.functor S) ⋯).pt

noncomputable def CategoryTheory.IsCardinalFiltered.toMax {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {K : Type u'} (S : K → J) (hS : HasCardinalLT K κ) (k : K) : S k ⟶ max S hS

If S : K → J is a family of objects of cardinality < κ in a κ-filtered category, this is a choice of map S k ⟶ max S hS for any k : K.

Equations

• CategoryTheory.IsCardinalFiltered.toMax S hS k = (CategoryTheory.IsCardinalFiltered.cocone (CategoryTheory.Discrete.functor S) ⋯).ι.app { as := k }

noncomputable def CategoryTheory.IsCardinalFiltered.coeq {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {K : Type v'} {j j' : J} (f : K → (j ⟶ j')) (hK : 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.

Equations

• CategoryTheory.IsCardinalFiltered.coeq f hK = (CategoryTheory.IsCardinalFiltered.cocone (CategoryTheory.Limits.parallelFamily f) ⋯).pt

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

Given a family of maps f : K → (j ⟶ j') in a κ-filtered category J, with HasCardinalLT K κ, and k : K, this is a choice of morphism j' ⟶ coeq f hK.

Equations

• CategoryTheory.IsCardinalFiltered.coeqHom f hK = (CategoryTheory.IsCardinalFiltered.cocone (CategoryTheory.Limits.parallelFamily f) ⋯).ι.app CategoryTheory.Limits.WalkingParallelFamily.one

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

Given a family of maps f : K → (j ⟶ j') in a κ-filtered category J, with HasCardinalLT K κ, this is a morphism j ⟶ coeq f hK which is equal to all compositions f k ≫ coeqHom f hK for k : K.

Equations

• CategoryTheory.IsCardinalFiltered.toCoeq f hK = (CategoryTheory.IsCardinalFiltered.cocone (CategoryTheory.Limits.parallelFamily f) ⋯).ι.app CategoryTheory.Limits.WalkingParallelFamily.zero

theorem CategoryTheory.IsCardinalFiltered.coeq_condition {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {K : Type v'} {j j' : J} (f : K → (j ⟶ j')) (hK : HasCardinalLT K κ) (k : K) : CategoryStruct.comp (f k) (coeqHom f hK) = toCoeq f hK

theorem CategoryTheory.IsCardinalFiltered.coeq_condition_assoc {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {K : Type v'} {j j' : J} (f : K → (j ⟶ j')) (hK : HasCardinalLT K κ) (k : K) {Z : J} (h : coeq f hK ⟶ Z) : CategoryStruct.comp (f k) (CategoryStruct.comp (coeqHom f hK) h) = CategoryStruct.comp (toCoeq f hK) h

theorem CategoryTheory.isFiltered_of_isCardinalDirected (J : Type u) [Category.{v, u} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] : IsFiltered J

theorem CategoryTheory.isCardinalFiltered_aleph0_iff (J : Type u) [Category.{v, u} J] : IsCardinalFiltered J Cardinal.aleph0 ↔ IsFiltered J

theorem CategoryTheory.isCardinalFiltered_preorder (J : Type w) [Preorder J] (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ (j : J), ∀ (k : K), s k ≤ j) : IsCardinalFiltered J κ

instance CategoryTheory.instIsCardinalFilteredToTypeOrd (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] : IsCardinalFiltered κ.ord.toType κ

instance CategoryTheory.isCardinalFiltered_under (J : Type u) [Category.{v, u} J] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J κ] (j₀ : J) : IsCardinalFiltered (Under j₀) κ