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

joelriou · 2026-05-21T11:03:26Z

Given a regular cardinal κ : Cardinal.{u}, we show that the category CardinalFilteredPoset κ of κ-directed partially ordered types (with order embeddings as morphisms) is a κ-accessible category.

depends on: [Merged by Bors] - feat(CategoryTheory): the category of κ-directed posets #39669

github-actions · 2026-05-21T11:04:43Z

PR summary 38bfba0ea1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ Hom.injective
+ Hom.le_iff_le
+ PropSet
+ cocone
+ hasCardinalLTWithTerminal
+ instance (S : Subtype J.PropSet) : HasTerminal S := S.prop.2
+ instance (S : Subtype J.PropSet) : IsCardinalFiltered S κ
+ instance : IsCardinalAccessibleCategory (CardinalFilteredPoset κ) κ
+ instance : IsCardinalFiltered (Subtype J.PropSet) κ
+ instance : IsDirectedOrder (Subtype J.PropSet)
+ instance : IsFiltered (Subtype J.PropSet) := isFiltered_of_isCardinalFiltered _ κ
+ instance : Nonempty (Subtype J.PropSet)
+ instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ)
+ isCardinalFilteredGenerator_hasCardinalLTWithTerminal
+ isCardinalPresentable_iff
+ isCardinalPresentable_iff'
+ isCardinalPresentable_of_hasCardinalLT_of_le
+ isColimitCocone
+ propSet_singleton

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 38bfba0).

+19 new declarations
−0 removed declarations

+CategoryTheory.CardinalFilteredPoset.Hom.injective
+CategoryTheory.CardinalFilteredPoset.Hom.le_iff_le
+CategoryTheory.CardinalFilteredPoset.PropSet
+CategoryTheory.CardinalFilteredPoset.cocone
+CategoryTheory.CardinalFilteredPoset.hasCardinalLTWithTerminal
+CategoryTheory.CardinalFilteredPoset.instEssentiallySmallHasCardinalLTWithTerminal
+CategoryTheory.CardinalFilteredPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredValSetPropSet
+CategoryTheory.CardinalFilteredPoset.instIsCardinalAccessibleCategory
+CategoryTheory.CardinalFilteredPoset.instIsCardinalFilteredElemCarrierObjPartOrdEmbIsCardinalFilteredValSetPropSet
+CategoryTheory.CardinalFilteredPoset.instIsCardinalFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet
+CategoryTheory.CardinalFilteredPoset.instIsDirectedOrderSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet
+CategoryTheory.CardinalFilteredPoset.instIsFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet
+CategoryTheory.CardinalFilteredPoset.instNonemptySubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet
+CategoryTheory.CardinalFilteredPoset.isCardinalFilteredGenerator_hasCardinalLTWithTerminal
+CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_iff
+CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_iff'
+CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_of_hasCardinalLT_of_le
+CategoryTheory.CardinalFilteredPoset.isColimitCocone
+CategoryTheory.CardinalFilteredPoset.propSet_singleton

Increase in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
4489	1	backward.defeqAttrib.useBackward
5660	1	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit 38bfba0ea1
Reference commit 7da7c276aa

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

…oset

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

…ardinal-directed-poset

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-dependent-issues · 2026-05-28T19:09:58Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory): the category of κ-directed posets #39669~~
By Dependent Issues (🤖). Happy coding!

…oset

…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 `< κ'`.

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

…oset

dagurtomas · 2026-06-17T23:35:22Z

Thanks!

maintainer merge

github-actions · 2026-06-17T23:35:53Z

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

riccardobrasca · 2026-06-18T10:22:39Z

Thanks!

bors merge

…39655) Given a regular cardinal `κ : Cardinal.{u}`, we show that the category `CardinalFilteredPoset κ` of `κ`-directed partially ordered types (with order embeddings as morphisms) is a `κ`-accessible category.

mathlib-bors · 2026-06-18T11:16:45Z

Pull request successfully merged into master.

Build succeeded:

…eanprover-community#39655) Given a regular cardinal `κ : Cardinal.{u}`, we show that the category `CardinalFilteredPoset κ` of `κ`-directed partially ordered types (with order embeddings as morphisms) is a `κ`-accessible category.

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

9d989b7

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

joelriou mentioned this pull request May 21, 2026

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

Open

19 tasks

whitespace

b72fcff

joelriou added the WIP Work in progress label May 21, 2026

joelriou added 6 commits May 21, 2026 18:33

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

41ee43e

…oset

characterization of presentable objects

db3987d

wip

bde3f62

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

882d14b

fix

a5a1782

leaving out some code here

96346f6

joelriou mentioned this pull request May 21, 2026

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

Closed

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 21, 2026

joelriou and others added 7 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

Merge remote-tracking branch 'origin/cardinal-directed-poset0' into c…

8ffa134

…ardinal-directed-poset

wip

f69a6cc

fix

a4c0062

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 28, 2026

joelriou added 3 commits May 29, 2026 15:08

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

ed21d1d

…oset

fix name

7ef6383

docstrings

c433904

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

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

dagurtomas reviewed Jun 16, 2026

View reviewed changes

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

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

dagurtomas added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 16, 2026

joelriou and others added 4 commits June 17, 2026 13:41

Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

46a35aa

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

Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

ca9ade2

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

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

69ba899

…oset

unif_hint

2c6ab44

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 17, 2026

joelriou added 3 commits June 17, 2026 15:00

fix

8bce378

removed disrupting unif_hint

33a45c4

removed parentheses

38bfba0

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

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 Jun 18, 2026

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

mathlib-bors Bot closed this Jun 18, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

[Merged by Bors] - feat(CategoryTheory): the κ-accessible category of κ-directed posets#39655
joelriou wants to merge 25 commits into
leanprover-community:masterfrom
joelriou:cardinal-directed-poset

joelriou commented May 21, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 21, 2026 •

edited

Loading

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-dependent-issues Bot commented May 28, 2026

Uh oh!

Uh oh!

Uh oh!

dagurtomas commented Jun 17, 2026

Uh oh!

github-actions Bot commented Jun 17, 2026

Uh oh!

riccardobrasca commented Jun 18, 2026

Uh oh!

mathlib-bors Bot commented Jun 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

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 38bfba0ea1

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-dependent-issues Bot commented May 28, 2026

Uh oh!

Uh oh!

Uh oh!

dagurtomas commented Jun 17, 2026

Uh oh!

github-actions Bot commented Jun 17, 2026

Uh oh!

riccardobrasca commented Jun 18, 2026

Uh oh!

mathlib-bors Bot commented Jun 18, 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