Skip to content

[Merged by Bors] - feat(SetTheory): the predicate HasCardinalLT#19959

Closed
joelriou wants to merge 5 commits intomasterfrom
set-theory-has-cardinal-lt
Closed

[Merged by Bors] - feat(SetTheory): the predicate HasCardinalLT#19959
joelriou wants to merge 5 commits intomasterfrom
set-theory-has-cardinal-lt

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Dec 14, 2024 •
edited
Loading

We introduce the universe-heterogeneous predicate HasCardinalLT X κ for X : Type u and κ : Cardinal.{v} saying that the cardinal of X is (strictly) less than κ. (This shall be used in the formalization of κ-filtered categories, which generalize filtered categories.)

Open in Gitpod

@joelriou joelriou added the t-set-theory Set theory label Dec 14, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 14, 2024 •
edited
Loading

PR summary 8adce59337

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.SetTheory.Cardinal.HasCardinalLT (new file) 650

Declarations diff

+ HasCardinalLT
+ hasCardinalLT_aleph0_iff
+ hasCardinalLT_iff_cardinal_mk_lt
+ hasCardinalLT_iff_of_equiv
+ of_injective
+ of_le
+ of_surjective
+ small

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/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).

This was referenced Dec 14, 2024
Closed
Closed
Closed
vihdzp
vihdzp suggested changes Dec 15, 2024
View reviewed changes
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't really like this idea. We already have a canonical way to write cardinal inequalities between different universes: if a : Cardinal.{u} and b : Cardinal.{v}, we write Cardinal.lift{v} a < Cardinal.lift.{u} b.

I could maybe instead support creating new predicates for universe-homogeneous <, ≤, and = for cardinals (and ordinals), which would surely make working with lift a bit easier. I am still very iffy about this however, since it would introduce a lot of boilerplate in exchange for reducing a bit of boilerplate elsewhere.

vihdzp
vihdzp reviewed Dec 15, 2024
View reviewed changes
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Dec 16, 2024

I don't really like this idea. We already have a canonical way to write cardinal inequalities between different universes: if a : Cardinal.{u} and b : Cardinal.{v}, we write Cardinal.lift{v} a < Cardinal.lift.{u} b.

The point is not to disturb the set theory API, but making it usable for other fields of mathematics. The notions of accessible/presentable objects in category theory require the notion of κ-filtered categories for a certain regular cardinal κ, and this involves types X whose cardinality is less than κ. I initially used Cardinal.mk X < κ, which would have been ok, but in category theory, we try to make things more universe polymorphic. Then, it is much more convenient for the user of the category theory API to see HasCardinalLT X κ rather than Cardinal.lift ... < Cardinal.lift ...: outside of the internals of the set theory API, in category theory files, we should not even need to know that the implementation uses Cardinal.lift...

@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Dec 16, 2024

I don't agree with the notion that Cardinal.lift is an implementation detail. There is a lot of API around it, to the point a bunch of theorems end up being stated in multiple forms depending on whether lift is used or not. This isn't just in category theory, but pretty much anywhere cardinals are used.

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Dec 16, 2024 •
edited
Loading

I don't agree with the notion that Cardinal.lift is an implementation detail. There is a lot of API around it, to the point a bunch of theorems end up being stated in multiple forms depending on whether lift is used or not. This isn't just in category theory, but pretty much anywhere cardinals are used.

The internals of the set theory API are very nice, but I do not see why all the details of it should be displayed to the category theory user.

dagurtomas
dagurtomas approved these changes Dec 16, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW, I think we should merge this, as its usefulness is evidenced by the subsequent series of PRs. A potential refactor of set theory API shouldn't block this, and can be thought about in parallel by those interested.

@dagurtomas
Copy link
Copy Markdown
Contributor

dagurtomas commented Dec 16, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 16, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 16, 2024
@dagurtomas
Copy link
Copy Markdown
Contributor

dagurtomas commented Dec 16, 2024

(discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/HasULift.20typeclass)

@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Dec 16, 2024

(after said discussion, I'm fine with merging this for now)

This was referenced Dec 16, 2024
Closed
Closed
Closed
This was referenced Dec 26, 2024
Closed
Open
@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Jan 13, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 13, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 13, 2025
@joelriou
feat(SetTheory): the predicate HasCardinalLT (#19959)
4f2a129 
We introduce the universe-heterogeneous predicate `HasCardinalLT X κ` for `X : Type u` and `κ : Cardinal.{v}` saying that the cardinal of `X` is (strictly) less than `κ`. (This shall be used in the formalization of `κ`-filtered categories, which generalize filtered categories.)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 13, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(SetTheory): the predicate HasCardinalLT [Merged by Bors] - feat(SetTheory): the predicate HasCardinalLT Jan 13, 2025
@mathlib-bors mathlib-bors bot closed this Jan 13, 2025
@mathlib-bors mathlib-bors bot deleted the set-theory-has-cardinal-lt branch January 13, 2025 10:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dagurtomas dagurtomas dagurtomas approved these changes

+1 more reviewer

@vihdzp vihdzp vihdzp requested changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-set-theory Set theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@joelriou @vihdzp @dagurtomas @ocfnash