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.

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

feat(RingTheory/LocalProperties): being projective can be checked locally on stalks #18131

Open
wants to merge 9 commits into
base: master
Choose a base branch
from

Conversation

erdOne
Copy link
Member

@erdOne erdOne commented Oct 23, 2024

... for finitely presented modules

Written at the AIM algebraic geometry workshop

Co-authored-by: David Swinarski


Open in Gitpod

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 23, 2024
Copy link

github-actions bot commented Oct 23, 2024

PR summary cc2212a3c7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.LocalProperties.Submodule 1188
Mathlib.RingTheory.LocalProperties.Projective 1207

Declarations diff

+ LinearMap.split_surjective_of_localization_maximal
+ Module.eq_of_localization_maximal
+ Module.eq_zero_of_localization_maximal
+ Module.projective_of_isLocalizedModule
+ Module.projective_of_localization_maximal
+ Module.projective_of_localization_maximal'
+ Module.subsingleton_of_localization_maximal
+ Submodule.eq_bot_of_localization_maximal
+ Submodule.eq_of_localization_maximal
+ Submodule.le_of_localization_maximal
+ Submodule.mem_of_localization_maximal
+ instance [Module.FinitePresentation R M] :

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.

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@erdOne erdOne added the workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry label Oct 23, 2024
Mathlib/Algebra/Module/FinitePresentation.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Projective.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Projective.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Projective.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Projective.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Projective.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Submodule.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Submodule.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Submodule.lean Outdated Show resolved Hide resolved
@chrisflav chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 26, 2024
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Oct 27, 2024
@erdOne
Copy link
Member Author

erdOne commented Oct 27, 2024

Thanks for the review!

@erdOne erdOne added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 27, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 29, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 29, 2024
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Oct 29, 2024
@erdOne erdOne removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 29, 2024
Mathlib/RingTheory/LocalProperties/Projective.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalProperties/Submodule.lean Outdated Show resolved Hide resolved
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
t-algebra Algebra (groups, rings, fields, etc) workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants