Skip to content

[Merged by Bors] - feat(RingTheory): localization and finiteness#14054

Closed
chrisflav wants to merge 3 commits intomasterfrom
chrisflav/finpres.2-pr
Closed

[Merged by Bors] - feat(RingTheory): localization and finiteness#14054
chrisflav wants to merge 3 commits intomasterfrom
chrisflav/finpres.2-pr

Conversation

@chrisflav
Copy link
Copy Markdown
Member

@chrisflav chrisflav commented Jun 23, 2024 •
edited
Loading

We show that Module.Finite is preserved under localizations and that if a module is finite after localizing at a spanning set of elements of the ring, it is finite.

The LocalizedModuleIntegers file is mostly a copy of IsLocalization.IsInteger.

Open in Gitpod

@chrisflav chrisflav added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 23, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 23, 2024 •
edited
Loading

PR summary e80f715913

Import changes

No significant changes to the import graph

Declarations diff

+ IsInteger
+ commonDenom
+ commonDenomOfFinset
+ exist_integer_multiples
+ exist_integer_multiples_of_finite
+ exist_integer_multiples_of_finset
+ exists_integer_multiple
+ finsetIntegerMultiple
+ finsetIntegerMultiple_image
+ integerMultiple
+ isInteger_add
+ isInteger_smul
+ isInteger_zero
+ map_integerMultiple
+ of_isLocalizedModule
+ of_localizationSpan
+ of_localizationSpan'
+ of_localizationSpan_finite
+ of_localizationSpan_finite'
+ smul_mem_finsetIntegerMultiple_span

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

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

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 23, 2024
erdOne
erdOne reviewed Jun 23, 2024
View reviewed changes
@erdOne erdOne added awaiting-author A reviewer has asked the author a question or requested changes. t-algebra Algebra (groups, rings, fields, etc) and removed awaiting-review labels Jun 23, 2024
@chrisflav chrisflav added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 23, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 23, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 23, 2024

Aside from the code duplication which makes me a bit sad, LGTM.
Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 23, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 23, 2024
kbuzzard
kbuzzard reviewed Jun 23, 2024
View reviewed changes
Mathlib/Algebra/Module/LocalizedModuleIntegers.lean Outdated

namespace IsLocalizedModule

section
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard Jun 23, 2024

Choose a reason for hiding this comment

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

Does this (and the end a few lines later) do anything?

Copy link
Copy Markdown
Member Author

@chrisflav chrisflav Jun 23, 2024

Choose a reason for hiding this comment

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

No, I removed it.

kbuzzard
kbuzzard approved these changes Jun 23, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

I'm not mad keen on IsInteger as a name, but I cannot think of a better name for the concept and so I guess it can be refactored later if I think of one. I don't really understand one of the sections so I've left a comment about it; feel free to delete the section if this is an oversight on your part.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2024

✌️ chrisflav 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 delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 23, 2024
@chrisflav
Copy link
Copy Markdown
Member Author

chrisflav commented Jun 23, 2024

Thanks for the reviews!

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jun 23, 2024
@chrisflav
feat(RingTheory): localization and finiteness (#14054)
f2d0448 
We show that `Module.Finite` is preserved under localizations and that if a module is finite after localizing at a spanning set of elements of the ring, it is finite.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory): localization and finiteness [Merged by Bors] - feat(RingTheory): localization and finiteness Jun 23, 2024
@mathlib-bors mathlib-bors bot closed this Jun 23, 2024
@mathlib-bors mathlib-bors bot deleted the chrisflav/finpres.2-pr branch June 23, 2024 22:05
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@chrisflav @kbuzzard
feat(RingTheory): localization and finiteness (#14054)
cdb7529 
We show that `Module.Finite` is preserved under localizations and that if a module is finite after localizing at a spanning set of elements of the ring, it is finite.
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@chrisflav @dagurtomas
feat(RingTheory): localization and finiteness (#14054)
a27e52e 
We show that `Module.Finite` is preserved under localizations and that if a module is finite after localizing at a spanning set of elements of the ring, it is finite.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

@kbuzzard kbuzzard kbuzzard approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@chrisflav @erdOne @kbuzzard