Skip to content

[Merged by Bors] - feat(SetTheory): regular cardinals have a least element#21780

Closed
joelriou wants to merge 8 commits intomasterfrom
jriou-cardinal-misc
Closed

[Merged by Bors] - feat(SetTheory): regular cardinals have a least element#21780
joelriou wants to merge 8 commits intomasterfrom
jriou-cardinal-misc

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Feb 12, 2025 •
edited
Loading

Ordinal.toTypeOrderBotOfPos is deprecated in favour of a new definition Ordinal.toTypeOrderBotOfPos which takes an assumption o ≠ 0. A similar definition is introduced for cardinals, and a lemma Cardinal.IsRegular.ne_zero is added. As a result, if c is a regular cardinal, then c.ord.toType has a least element.

Open in Gitpod

@joelriou joelriou added t-order Order theory t-set-theory Set theory labels Feb 12, 2025
@joelriou joelriou mentioned this pull request Feb 12, 2025
Closed
21 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 12, 2025 •
edited
Loading

PR summary b5510cc486

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsRegular.ne_zero
++ toTypeOrderBot

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

b-mehta
b-mehta reviewed Feb 12, 2025
View reviewed changes
@b-mehta b-mehta requested a review from vihdzp February 12, 2025 19:25
@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Feb 12, 2025

Ordinal.toType is very strong code smell, and it's only ever something you use when you absolutely need a type in the same universe (see e.g. the definition of PGame.nim). Is there a reason you can't just write down Iio c.ord instead?

@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Feb 12, 2025

I am not certain - Joël can correct me - but I think this is a case where remaining in the same universe is important, since the definition of (co)limits in a category does need to be specific about its universe levels. (If I'm mistaken however, and we don't need to stay in the same universe, then I agree Iio could be better).

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Feb 12, 2025

Indeed, Bhavik is right. In my application, I have an auxiliary universe parameter w, and I assume that I have a certain regular cardinal c : Cardinal.{w} precisely so that I can take the corresponding well ordered type in Type w. I would not mind if there was a better phrasing for c.ord.toType, but it has to be in Type w.

vihdzp
vihdzp reviewed Feb 12, 2025
View reviewed changes
Mathlib/SetTheory/Ordinal/Basic.lean Outdated
exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩

/-- If a cardinal `c` is non zero, then `c.ord.toType` has a least element. -/
noncomputable def orderBotToType (c : Cardinal) (hc : c ≠ 0) :
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp Feb 12, 2025

Choose a reason for hiding this comment

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

This should match Ordinal.toTypeOrderBotOfPos in both name and arguments. Though, I wouldn't mind changing the latter into this, since its current name is more unwieldy and it's slightly easier to get x ≠ 0 than 0 < x (particularly now that we don't yet have a CanonicallyOrderedAdd instance for Ordinal).

Copy link
Copy Markdown
Contributor

@b-mehta b-mehta Feb 12, 2025

Choose a reason for hiding this comment

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

Yeah, I think taking in the != 0 argument is better in both cases.
To me orderBotToType is a slightly better name, it certainly matches the symbol read of the statement. Would you mind adjusting Ordinal.toTypeOrderBotOfPos closer to the name here?

Copy link
Copy Markdown
Contributor Author

@joelriou joelriou Feb 13, 2025

Choose a reason for hiding this comment

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

I have deprecated Ordinal.toTypeOrderBotOfPos, and I think the new definition may just be named Ordinal.toTypeOrderBot.

@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 13, 2025
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 13, 2025
b-mehta
b-mehta approved these changes Feb 13, 2025
View reviewed changes
@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Feb 13, 2025

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 13, 2025

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 13, 2025
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Feb 13, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 13, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 13, 2025
@joelriou
feat(SetTheory): regular cardinals have a least element (#21780)
2278a54 
`Ordinal.toTypeOrderBotOfPos` is deprecated in favour of a new definition `Ordinal.toTypeOrderBotOfPos` which takes an assumption `o ≠ 0`. A similar definition is introduced for cardinals, and a lemma `Cardinal.IsRegular.ne_zero` is added. As a result, if `c` is a regular cardinal, then `c.ord.toType` has a least element. 



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 13, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(SetTheory): regular cardinals have a least element [Merged by Bors] - feat(SetTheory): regular cardinals have a least element Feb 13, 2025
@mathlib-bors mathlib-bors bot closed this Feb 13, 2025
@mathlib-bors mathlib-bors bot deleted the jriou-cardinal-misc branch February 13, 2025 15:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta approved these changes

+1 more reviewer

@vihdzp vihdzp vihdzp left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-order Order theory t-set-theory Set theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @vihdzp @b-mehta