Theorems · Theorem · category theory

CategoryTheory.IsCardinalFiltered.of_final

∀ {J₁ : Type u} [inst : CategoryTheory.Category.{v, u} J₁] {J₂ : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J₂]
  (F : CategoryTheory.Functor J₁ J₂) [F.Final] (κ : Cardinal.{w}) [inst_3 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J₁ κ], CategoryTheory.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 (κ = ℵ₀).

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.FinalFactCategoryTheory.IsCardinalFiltered