Theorems · Inductive type · category theory

CategoryTheory.IsCardinalFiltered

(J : Type u) → [CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

69 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryFact