Theorems · Theorem · category theory

CategoryTheory.IsCardinalFilteredGenerator.of_isDense

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} J] [CategoryTheory.EssentiallySmall.{w, v', u'} J]
  (F : CategoryTheory.Functor J C) [F.IsDense] (κ : Cardinal.{w}) [inst_5 : Fact κ.IsRegular]
  [∀ (j : J), CategoryTheory.IsCardinalPresentable (F.obj j) κ]
  [∀ (X : C), CategoryTheory.IsCardinalFiltered (CategoryTheory.CostructuredArrow F X) κ],
  (⊤.map F).IsCardinalFilteredGenerator κ

Defined in

Mathlib.CategoryTheory.Presentable.StrongGenerator

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmallCategoryTheory.CategoryCategoryTheory.EssentiallySmallCategoryTheory.Functor.IsDenseFactCategoryTheory.IsCardinalPresentableCategoryTheory.IsCardinalFiltered