Theorems · Theorem · category theory

PartOrdEmb.Limits.CoconePt.isCardinalFiltered_pt

∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : Type u} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsCardinalFiltered J κ] {F : CategoryTheory.Functor J PartOrdEmb}
  {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))}
  (hc : CategoryTheory.Limits.IsColimit c),
  (∀ (j : J), CategoryTheory.IsCardinalFiltered (↑(F.obj j)) κ) →
    CategoryTheory.IsCardinalFiltered (PartOrdEmb.Limits.CoconePt hc) κ

Defined in

Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactCategoryTheory.SmallCategoryCategoryTheory.IsCardinalFiltered