Skip to content

[Merged by Bors] - feat(FieldTheory/Relrank): Relative rank of subfields and intermediate fields#14987

Closed
acmepjz wants to merge 12 commits intomasterfrom
acmepjz_if_relrank
Closed

[Merged by Bors] - feat(FieldTheory/Relrank): Relative rank of subfields and intermediate fields#14987
acmepjz wants to merge 12 commits intomasterfrom
acmepjz_if_relrank

Conversation

@acmepjz
Copy link
Copy Markdown
Collaborator

@acmepjz acmepjz commented Jul 21, 2024 •
edited
Loading

@acmepjz acmepjz added help-wanted The author needs attention to resolve issues WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Jul 21, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 21, 2024 •
edited
Loading

PR summary ccbd6fe1e5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.FieldTheory.Relrank 1356

Declarations diff

+ finrank_bot_mul_relfinrank
+ rank_bot_mul_relrank
+ relfinrank_bot_left
+ relfinrank_bot_right
+ relfinrank_dvd_finrank_bot
+ relrank_bot_left
+ relrank_bot_right
+ relrank_dvd_rank_bot
++ finrank_comap
++ inf_relfinrank_left
++ inf_relfinrank_right
++ inf_relrank_left
++ inf_relrank_right
++ lift_rank_comap
++ lift_relrank_comap
++ lift_relrank_comap_comap_eq_lift_relrank_inf
++ lift_relrank_comap_comap_eq_lift_relrank_of_le
++ lift_relrank_comap_comap_eq_lift_relrank_of_surjective
++ lift_relrank_map_map
++ rank_comap
++ relfinrank
++ relfinrank_comap
++ relfinrank_comap_comap_eq_relfinrank_inf
++ relfinrank_comap_comap_eq_relfinrank_of_le
++ relfinrank_comap_comap_eq_relfinrank_of_surjective
++ relfinrank_dvd_finrank_top_of_le
++ relfinrank_dvd_of_le_left
++ relfinrank_eq_finrank_of_le
++ relfinrank_eq_of_inf_eq
++ relfinrank_eq_one_of_le
++ relfinrank_eq_toNat_relrank
++ relfinrank_inf_mul_relfinrank
++ relfinrank_inf_mul_relfinrank_of_le
++ relfinrank_map_map
++ relfinrank_mul_finrank_top
++ relfinrank_mul_relfinrank
++ relfinrank_mul_relfinrank_eq_inf_relfinrank
++ relfinrank_self
++ relfinrank_top_left
++ relfinrank_top_right
++ relrank
++ relrank_comap
++ relrank_comap_comap_eq_relrank_inf
++ relrank_comap_comap_eq_relrank_of_le
++ relrank_comap_comap_eq_relrank_of_surjective
++ relrank_dvd_of_le_left
++ relrank_dvd_rank_top_of_le
++ relrank_eq_of_inf_eq
++ relrank_eq_one_of_le
++ relrank_eq_rank_of_le
++ relrank_inf_mul_relrank
++ relrank_inf_mul_relrank_of_le
++ relrank_map_map
++ relrank_mul_rank_top
++ relrank_mul_relrank
++ relrank_mul_relrank_eq_inf_relrank
++ relrank_self
++ relrank_top_left
++ relrank_top_right

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.

@tb65536
Copy link
Copy Markdown
Contributor

tb65536 commented Jul 22, 2024 •
edited
Loading

Is it certain that we want this to be cardinal-valued rather than nat-valued? Personally, I feel like the convenience of nat-valued would outweigh the benefit of distinguishing countable vs uncountable degree extensions (my impression is that for infinite degree extensions, you usually care more about transcendence degree than the usual degree as a cardinal).

@acmepjz
Copy link
Copy Markdown
Collaborator Author

acmepjz commented Jul 22, 2024 •
edited
Loading

Is it certain that we want this to be cardinal-valued rather than nat-valued? Personally, I feel like the convenience of nat-valued would outweigh the benefit of distinguishing countable vs uncountable degree extensions (my impression is that for infinite degree extensions, you usually care more about transcendence degree than the usual degree as a cardinal).

Personally I'd like to make relrank Cardinal-valued, following the naming of rank and finrank. We can also define relfinrank or finrelrank which is Nat-valued.

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jul 22, 2024

I think I agree with @tb65536 that Nat-valued is much more useful. I also agree with @acmepjz that this creates a bit of an inconsistency naming-wise. But maybe we should fix that be renaming rank to cardinal_rank (crank 🤣) or something like that, so that finrank can be moved to rank.
Since relrank for subgroups is already Nat-valued, I think it doesn't hurt to do the same here.

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 27, 2024
@acmepjz acmepjz changed the title feat(FieldTheory/Relrank): Relative rank of intermediate fields feat(FieldTheory/Relrank): Relative rank of subfields and intermediate fields Jul 28, 2024
@acmepjz acmepjz removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Jul 30, 2024
@acmepjz acmepjz marked this pull request as ready for review July 30, 2024 19:27
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 31, 2024
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 31, 2024
@acmepjz acmepjz added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 3, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 18, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Oct 18, 2024

This PR/issue depends on:

@acmepjz acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 26, 2024
tb65536
tb65536 reviewed Oct 26, 2024
View reviewed changes
alreadydone
alreadydone reviewed Oct 26, 2024
View reviewed changes
@acmepjz acmepjz mentioned this pull request Nov 8, 2024
Closed
alreadydone
alreadydone approved these changes Nov 12, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

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

Just a few minor questions

alreadydone
alreadydone reviewed Nov 13, 2024
View reviewed changes
@alreadydone
Copy link
Copy Markdown
Contributor

alreadydone commented Nov 13, 2024

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 13, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 13, 2024
jcommelin
jcommelin reviewed Nov 14, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 14, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 14, 2024
@acmepjz
feat(FieldTheory/Relrank): Relative rank of subfields and intermediat…
25c4cee 
…e fields (#14987)

We define `Subfield.relrank A B` and `IntermediateField.relrank A B`, which is `[B : A ⊓ B]`, in particular, when `A ≤ B` it is `[B : A]`, the degree of the field extension `B / A`. This is similar to `Subgroup.relindex`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 14, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(FieldTheory/Relrank): Relative rank of subfields and intermediate fields [Merged by Bors] - feat(FieldTheory/Relrank): Relative rank of subfields and intermediate fields Nov 14, 2024
@mathlib-bors mathlib-bors bot closed this Nov 14, 2024
@mathlib-bors mathlib-bors bot deleted the acmepjz_if_relrank branch November 14, 2024 04:36
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@acmepjz @TobiasLeichtfried
feat(FieldTheory/Relrank): Relative rank of subfields and intermediat…
8ce6630 
…e fields (#14987)

We define `Subfield.relrank A B` and `IntermediateField.relrank A B`, which is `[B : A ⊓ B]`, in particular, when `A ≤ B` it is `[B : A]`, the degree of the field extension `B / A`. This is similar to `Subgroup.relindex`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@alreadydone alreadydone alreadydone approved these changes

@jcommelin jcommelin jcommelin left review comments

@tb65536 tb65536 tb65536 left review comments

Assignees

@alreadydone alreadydone

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@acmepjz @tb65536 @jcommelin @mathlib4-dependent-issues-bot @alreadydone