Theorems · Definition · category theory

CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet

{κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    {J : CategoryTheory.CardinalDirectedPoset κ} →
      (P : Set ↑J.obj → Prop) →
        [inst_1 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] →
          CategoryTheory.Limits.Cocone (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet P)

Given a predicate P : Set J.obj → Prop on the underlying type of J : CardinalDirectedPoset κ such that all the subsets satisfying P are κ-filtered, this is the cocone with point J given by all the inclusions of the subsets satisfying P.

Defined in

Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Cited by

2 results in Mathlib

Foundations

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

Assumes

FactCategoryTheory.IsCardinalFiltered