κ-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. See isCardinalFiltered_iff for a more concrete characterization of κ-filtered categories.

• 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.IsCardinalFiltered.wideSpan {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] {ι : Type v'} {j : J} {k : ι → J} (f : (i : ι) → j ⟶ k i) (hι : HasCardinalLT ι κ) : ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), CategoryStruct.comp (f i) (a i) = b

Variant of IsFiltered.span for κ-filtered categories.

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

theorem CategoryTheory.IsCardinalFiltered.nonempty (J : Type u) [Category.{v, u} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] : Nonempty 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₀) κ

instance CategoryTheory.isCardinalFiltered_prod (J₁ : Type u) (J₂ : Type u') [Category.{v, u} J₁] [Category.{v', u'} J₂] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J₁ κ] [IsCardinalFiltered J₂ κ] : IsCardinalFiltered (J₁ × J₂) κ

instance CategoryTheory.isCardinalFiltered_pi {ι : Type u'} (J : ι → Type u) [(i : ι) → Category.{v, u} (J i)] (κ : Cardinal.{w}) [Fact κ.IsRegular] [∀ (i : ι), IsCardinalFiltered (J i) κ] : IsCardinalFiltered ((i : ι) → J i) κ

theorem CategoryTheory.isCardinalFiltered_iff_aux₁ {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} (h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty (j i ⟶ k)) (h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), CategoryStruct.comp (f i) a = b) {ι : Type w} {j : J} {k : ι → J} (f : (i : ι) → j ⟶ k i) (hι : HasCardinalLT ι κ) : ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), CategoryStruct.comp (f i) (a i) = b

theorem CategoryTheory.isCardinalFiltered_iff_aux₂ {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty (j i ⟶ k)) (h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), CategoryStruct.comp (f i) a = b) {ι : Type w} {j : ι → J} {k : J} (f₁ f₂ : (i : ι) → j i ⟶ k) (hι : HasCardinalLT ι κ) : ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), CategoryStruct.comp (f₁ i) a = CategoryStruct.comp (f₂ i) a

theorem CategoryTheory.isCardinalFiltered_iff (J : Type u) [Category.{v, u} J] (κ : Cardinal.{w}) [Fact κ.IsRegular] : IsCardinalFiltered J κ ↔ (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty (j i ⟶ k)) ∧ ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), CategoryStruct.comp (f i) a = b

A category is κ-filtered iff

1. any family of objects of cardinality < κ admits a map towards a common object, and
2. any family of morphisms j ⟶ k of cardinality < κ (between fixed objects j and k) can be coequalized by a suitable morphism k ⟶ l.

theorem CategoryTheory.IsCardinalFiltered.multicoequalizer {J : Type u} [Category.{v, u} J] {κ : Cardinal.{w}} [Fact κ.IsRegular] [IsCardinalFiltered J κ] {ι : Type v'} {j : ι → J} {k : J} (f₁ f₂ : (i : ι) → j i ⟶ k) (hι : HasCardinalLT ι κ) : ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), CategoryStruct.comp (f₁ i) a = CategoryStruct.comp (f₂ i) a

theorem CategoryTheory.IsCardinalFiltered.of_final {J₁ : Type u} [Category.{v, u} J₁] {J₂ : Type u'} [Category.{v', u'} J₂] (F : Functor J₁ J₂) [F.Final] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J₁ κ] : IsCardinalFiltered J₂ κ

If F : J₁ ⥤ J₂ is final and J₁ is κ-filtered, then J₂ is also κ-filtered. See also IsFiltered.of_final (in CategoryTheory.Limits.Final) for the particular case of filtered categories (κ = ℵ₀).

theorem CategoryTheory.Limits.IsTerminal.isCardinalFiltered {J : Type u} [Category.{v, u} J] {X : J} (hX : IsTerminal X) (κ : Cardinal.{w}) [Fact κ.IsRegular] : IsCardinalFiltered J κ

theorem CategoryTheory.isCardinalFiltered_of_hasTerminal (J : Type u) [Category.{v, u} J] [Limits.HasTerminal J] (κ : Cardinal.{w}) [Fact κ.IsRegular] : IsCardinalFiltered J κ