[Merged by Bors] - feat(CategoryTheory): the category of κ-directed posets by joelriou · Pull Request #39669 · leanprover-community/mathlib4

joelriou · 2026-05-21T19:22:40Z

Given a regular cardinal κ : Cardinal.{u}, we define the category CardinalFilteredPoset κ of κ-directed partially ordered types (with order embeddings as morphisms). In a future PR #39655, we shall show that it is a κ-accessible category.
In this PR, we also show that if J : CardinalFilteredPoset κ, the object J.withTop obtained by adding a top element is a κ'-filtered colimit of objects of cardinality < κ' (when κ' is a regular cardinal such that κ ≤ κ'). This shall be used in #39655 in order to characterize κ'-presentable objects in CardinalFilteredPoset κ as the objects that are of cardinality < κ'.

github-actions · 2026-05-21T19:24:03Z

PR summary 0271eb7d56

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset` (new file)	1010

Declarations diff

+ CardinalFilteredPoset
+ CardinalFilteredPoset.ι
+ PropSetWithTop
+ coconeWithTop
+ exists_mem_propSetWithTop
+ instance (A : Type u) [SmallCategory A] [IsCardinalFiltered A κ] :
+ instance (J : CardinalFilteredPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] :
+ instance (J : CardinalFilteredPoset κ) : IsCardinalFiltered J.obj κ := J.property
+ instance (J : CardinalFilteredPoset κ) : IsFiltered J.obj
+ instance (J : CardinalFilteredPoset κ) : Nonempty J.obj := IsFiltered.nonempty
+ instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] :
+ instance (S : Subtype (J.PropSetWithTop κ')) : HasTerminal S
+ instance (S : Subtype (J.PropSetWithTop κ')) : IsCardinalFiltered S κ
+ instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms
+ instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms
+ instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ
+ instance : IsCardinalFiltered (Subtype (J.PropSetWithTop κ')) κ'
+ instance : IsDirectedOrder (Subtype (J.PropSetWithTop κ'))
+ instance : IsFiltered (Subtype (J.PropSetWithTop κ'))
+ instance : Nonempty (Subtype (J.PropSetWithTop κ'))
+ instance : ReflectsColimitsOfShape J (forget PartOrdEmb.{u})
+ isCardinalFiltered
+ isCardinalFiltered_iff
+ isCardinalFiltered_pt
+ isColimitCoconeOfPredicateSet
+ isColimitCoconeWithTop
+ isColimitOfPredicateSet
+ of
+ orderIsoEquivIso
+ orderIsoOfIso
+ propSetWithTop_pair
+ withTop
++ coconeOfPredicateSet
++ functorOfPredicateSet

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

dagurtomas

Thanks!

maintainer delegate

github-actions · 2026-05-21T20:46:50Z

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

joelriou · 2026-05-22T08:19:35Z

Downstream developments require some refactoring, so that this will have to be reviewed again later (I am sorry for this).

joelriou · 2026-05-22T09:31:13Z

The only significant difference with the previously maintainer merged version of this PR is in the commit f5bd8f0 which introduces helpers to construct (filtered) colimits in PartOrdEmb and CardinalFilteredPoset (given a predicate P on subsets of a partial ordered type T, there are conditions that allow to show that T is the colimit of the subset satisfying P). This added API makes it easier to construct the colimit cocone coconeWithTop. (This API will be reused in subsequent PR.)

dagurtomas

Thanks! Again:

maintainer delegate

github-actions · 2026-05-28T16:00:25Z

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

…oset0

riccardobrasca · 2026-05-28T18:16:53Z

Thanks!

bors merge

Given a regular cardinal `κ : Cardinal.{u}`, we define the category `CardinalFilteredPoset κ` of `κ`-directed partially ordered types (with order embeddings as morphisms). In a future PR #39655, we shall show that it is a `κ`-accessible category. In this PR, we also show that if `J : CardinalFilteredPoset κ`, the object `J.withTop` obtained by adding a top element is a `κ'`-filtered colimit of objects of cardinality `< κ'` (when `κ'` is a regular cardinal such that `κ ≤ κ'`). This shall be used in #39655 in order to characterize `κ'`-presentable objects in `CardinalFilteredPoset κ` as the objects that are of cardinality `< κ'`.

mathlib-bors · 2026-05-28T18:53:05Z

Pull request successfully merged into master.

Build succeeded:

…ommunity#39669) Given a regular cardinal `κ : Cardinal.{u}`, we define the category `CardinalFilteredPoset κ` of `κ`-directed partially ordered types (with order embeddings as morphisms). In a future PR leanprover-community#39655, we shall show that it is a `κ`-accessible category. In this PR, we also show that if `J : CardinalFilteredPoset κ`, the object `J.withTop` obtained by adding a top element is a `κ'`-filtered colimit of objects of cardinality `< κ'` (when `κ'` is a regular cardinal such that `κ ≤ κ'`). This shall be used in leanprover-community#39655 in order to characterize `κ'`-presentable objects in `CardinalFilteredPoset κ` as the objects that are of cardinality `< κ'`.

joelriou added 2 commits May 21, 2026 21:21

feat(CategoryTheory): the category of κ-directed posets

882d14b

fix

a5a1782

joelriou added the t-category-theory Category theory label May 21, 2026

This was referenced May 21, 2026

[Merged by Bors] - feat(CategoryTheory): the κ-accessible category of κ-directed posets #39655

Closed

feat(CategoryTheory/Presentable): the uniformization theorem #31018

Open

leaving out some code here

96346f6

dagurtomas reviewed May 21, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 21, 2026

joelriou and others added 4 commits May 21, 2026 22:50

Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

69d6fc5

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

7ce5d15

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

8702bdc

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

suggestions by @dagurtomas

4981f8b

joelriou added WIP Work in progress and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 22, 2026

joelriou added 2 commits May 22, 2026 11:24

better API for colimits in PartOrdEmb

f5bd8f0

fix

a4f65b1

fix

6e9afd1

joelriou removed the WIP Work in progress label May 22, 2026

mathlib-triage Bot assigned robin-carlier May 24, 2026

dagurtomas self-requested a review May 28, 2026 06:55

dagurtomas reviewed May 28, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean Outdated

Comment thread Mathlib/Order/Category/PartOrdEmb.lean Outdated

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 28, 2026

joelriou and others added 3 commits May 28, 2026 18:11

Update Mathlib/Order/Category/PartOrdEmb.lean

a207be2

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

d459607

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

Merge remote-tracking branch 'origin/master' into cardinal-directed-p…

1e5548a

…oset0

fix

0271eb7

mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 28, 2026

mathlib-bors Bot changed the title ~~feat(CategoryTheory): the category of κ-directed posets~~ [Merged by Bors] - feat(CategoryTheory): the category of κ-directed posets May 28, 2026

mathlib-bors Bot closed this May 28, 2026

Uh oh!

Conversation

joelriou commented May 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0271eb7d56

Import changes for modified files

Declarations diff

Uh oh!

dagurtomas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026

Uh oh!

joelriou commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joelriou commented May 22, 2026

Uh oh!

dagurtomas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented May 28, 2026

Uh oh!

riccardobrasca commented May 28, 2026

Uh oh!

mathlib-bors Bot commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

joelriou commented May 21, 2026 •

edited

Loading

github-actions Bot commented May 21, 2026 •

edited

Loading

joelriou commented May 22, 2026 •

edited

Loading