Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - move: Rearrange basic algebraic subobject #11104

Closed
wants to merge 53 commits into from
Closed

[Merged by Bors] - move: Rearrange basic algebraic subobject #11104

wants to merge 53 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Mar 2, 2024 •
edited

For Foo an algebraic typeclass, the basic theory of Subfoo currently is under FooTheory.Subfoo. This is in contradiction to other kinds of subobjects, eg order theoretic ones.

This PR moves that basic theory to Algebra.Foo.Subfoo instead.

Zulip

Open in Gitpod

@YaelDillies
move: Rearrange Subfield material
23bcddc 
Move
* `FieldTheory.Subfield` to `Algebra.Field.Subfield` because there is nothing field-theoretic happening there
* `FieldTheory.Subfield.Order` to `Algebra.Order.Field.Subfield` for the same reason

Split `Topology.Algebra.Field` into
* `Topology.Algebra.Field.Basic` for the basic properties of topological fields
* `Topology.Algebra.Field.Subfield` for the properties of subfields of topological fields. I credit Xavier for leanprover-community/mathlib#17212
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR awaiting-CI t-topology Topological spaces, uniform spaces, metric spaces, filters t-algebra Algebra (groups, rings, fields etc) labels Mar 2, 2024
@eric-wieser
Copy link
Member

  • FieldTheory.Subfield to Algebra.Field.Subfield because there is nothing field-theoretic happening there

This isn't consistent with how Subring, Submonoid, Subgroup are handled; all reside in the corresponding *Theory folder

@YaelDillies
Copy link
Collaborator Author

YaelDillies commented Mar 2, 2024 •
edited

Good point. I'm not sure I like the way subobjects are dealt with, then.

But feel free to do whatever you want with this PR (close it, edit it, merge it). I'm not fussed.

eric-wieser
eric-wieser previously requested changes Mar 2, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

My inclination would be to close this. If we're going to split things relating to subobjects, we should try to be consistent across all subobjects in the way we do so. This PR just makes things less consistent.

Mathlib/Topology/Algebra/Field/Subfield.lean Outdated Show resolved Hide resolved
@eric-wieser
Copy link
Member

Good point. I'm not sure I like the way subobjects are dealt with, then.

Perhaps worth a Zulip thread?

@semorrison
Copy link
Contributor

If Eric wants to nix the move, that doesn't seem any obstacle to the main point of this PR, which is to split Topology.Algebra.Field, no?

@eric-wieser
Copy link
Member

which is to split Topology.Algebra.Field

I'm not opposed to this, but I don't think we should do it without also splitting Topology.Algebra.Ring to not mention Subring, etc

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 4, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 5, 2024
@semorrison
Copy link
Contributor

I'm not opposed to this, but I don't think we should do it without also splitting Topology.Algebra.Ring to not mention Subring, etc

Seems like a recipe for not getting anything done!

@eric-wieser
Copy link
Member

Seems like a recipe for not getting anything done!

Yes, I think leaving files unsplit is better than splitting them inconsistently; the latter just creates more work downstream and makes it harder to work out where to put things

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 8, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 8, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 17, 2024
@YaelDillies
Copy link
Collaborator Author

This PR is now about moving basic algebraic subobject material from the FooTheory folders to Algebra.Foo.SubFoo.

@YaelDillies YaelDillies changed the title move: Rearrange Subfield material move: Rearrange basic algebraic subobject Mar 18, 2024
@YaelDillies YaelDillies added awaiting-CI and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Mar 18, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 18, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Apr 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 2, 2024
Ruben-VandeVelde
Ruben-VandeVelde approved these changes May 3, 2024
View reviewed changes
Mathlib/Deprecated/Subgroup.lean Outdated Show resolved Hide resolved
Mathlib/Deprecated/Subring.lean Outdated Show resolved Hide resolved
Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean Outdated Show resolved Hide resolved
@Ruben-VandeVelde
Copy link
Collaborator

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented May 3, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 3, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 3, 2024
@YaelDillies @Ruben-VandeVelde
move: Rearrange basic algebraic subobject (#11104)
eaa2357 
For `Foo` an algebraic typeclass, the basic theory of `Subfoo` currently is under `FooTheory.Subfoo`. This is in contradiction to other kinds of subobjects, eg order theoretic ones.

This PR moves that basic theory to `Algebra.Foo.Subfoo` instead.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Location.20of.20algebraic.20subobjects)



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@mathlib-bors
Copy link

mathlib-bors bot commented May 3, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request May 3, 2024
@YaelDillies @Ruben-VandeVelde
move: Rearrange basic algebraic subobject (#11104)
5bcbd8b 
For `Foo` an algebraic typeclass, the basic theory of `Subfoo` currently is under `FooTheory.Subfoo`. This is in contradiction to other kinds of subobjects, eg order theoretic ones.

This PR moves that basic theory to `Algebra.Foo.Subfoo` instead.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Location.20of.20algebraic.20subobjects)



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@mathlib-bors
Copy link

mathlib-bors bot commented May 3, 2024

Build failed:

@Vierkantor
Copy link
Contributor

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented May 3, 2024

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

@Vierkantor
Copy link
Contributor

Let's try that again:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request May 3, 2024
@YaelDillies @Ruben-VandeVelde @Vierkantor
move: Rearrange basic algebraic subobject (#11104)
efb7091 
For `Foo` an algebraic typeclass, the basic theory of `Subfoo` currently is under `FooTheory.Subfoo`. This is in contradiction to other kinds of subobjects, eg order theoretic ones.

This PR moves that basic theory to `Algebra.Foo.Subfoo` instead.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Location.20of.20algebraic.20subobjects)



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
@mathlib-bors
Copy link

mathlib-bors bot commented May 3, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title move: Rearrange basic algebraic subobject [Merged by Bors] - move: Rearrange basic algebraic subobject May 3, 2024
@mathlib-bors mathlib-bors bot closed this May 3, 2024
@mathlib-bors mathlib-bors bot deleted the move_subfield branch May 3, 2024 14:30
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@YaelDillies @Ruben-VandeVelde
@Vierkantor @apnelson1
move: Rearrange basic algebraic subobject (#11104)
acbcf2a 
For `Foo` an algebraic typeclass, the basic theory of `Subfoo` currently is under `FooTheory.Subfoo`. This is in contradiction to other kinds of subobjects, eg order theoretic ones.

This PR moves that basic theory to `Algebra.Foo.Subfoo` instead.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Location.20of.20algebraic.20subobjects)



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
callesonne pushed a commit that referenced this pull request May 16, 2024
@YaelDillies @Ruben-VandeVelde
@Vierkantor @callesonne
move: Rearrange basic algebraic subobject (#11104)
5a1a7e3 
For `Foo` an algebraic typeclass, the basic theory of `Subfoo` currently is under `FooTheory.Subfoo`. This is in contradiction to other kinds of subobjects, eg order theoretic ones.

This PR moves that basic theory to `Algebra.Foo.Subfoo` instead.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Location.20of.20algebraic.20subobjects)



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
@kbuzzard kbuzzard mentioned this pull request Jun 2, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@github-actions github-actions[bot] github-actions left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
delegated maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc) t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@YaelDillies @eric-wieser @semorrison @Ruben-VandeVelde @riccardobrasca @Vierkantor @leanprover-community-mathlib4-bot