Skip to content

[Merged by Bors] - feat: add the definition of OrzechProperty#13322

Closed
acmepjz wants to merge 6 commits intomasterfrom
acmepjz_orzech_def
Closed

[Merged by Bors] - feat: add the definition of OrzechProperty#13322
acmepjz wants to merge 6 commits intomasterfrom
acmepjz_orzech_def

Conversation

@acmepjz
Copy link
Copy Markdown
Collaborator

@acmepjz acmepjz commented May 28, 2024 •
edited
Loading

This is part one of #12076.

OrzechProperty R is a type class stating that R satisfies the following property: for any finitely generated R-module M, any surjective homomorphism f : N → M from a submodule N of M to M is injective.

We stated some basic results about OrzechProperty and proved that it implies StrongRankCondition.

Open in Gitpod

discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312076.20Orzech's.20theorem

@acmepjz acmepjz added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels May 28, 2024
@acmepjz acmepjz mentioned this pull request May 28, 2024
Closed
2 tasks
@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 May 28, 2024
kbuzzard
kbuzzard approved these changes May 28, 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.

LGTM! I left some comments which expose my ignorance.

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented May 29, 2024

Thanks for splitting the PR!

Looks good to me. If @AntoineChambert-Loir also agrees, let's get this merged.

bors d=AntoineChambert-Loir

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 29, 2024

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

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels May 29, 2024
AntoineChambert-Loir
AntoineChambert-Loir reviewed May 31, 2024
View reviewed changes
@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

AntoineChambert-Loir commented May 31, 2024

I am not convinced about two minor points.

  • the docstrings duplicate themselves and announce future work at improper places
    (but they may change once the rest of the work on the Orzech property is added)
  • the IBN file is short, the Orzech property is not that long, and everything is about the same kind of ideas.
    So can't all of this go into a single file (IBN.lean, for example)?

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 31, 2024
@acmepjz
Copy link
Copy Markdown
Collaborator Author

acmepjz commented May 31, 2024

the IBN file is short, the Orzech property is not that long, and everything is about the same kind of ideas.
So can't all of this go into a single file (IBN.lean, for example)?

I'm not sure about this, as we discussed in #12076 (comment) and #12076 (comment). I think the reason of Orzech go to a single file is that it needs fewer imports, and maybe we can define Orzech property for modules, which, if defined, is belong to Orzech file.

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 31, 2024
@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

AntoineChambert-Loir commented May 31, 2024

good!

@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

AntoineChambert-Loir commented May 31, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request May 31, 2024
@acmepjz
feat: add the definition of OrzechProperty (#13322)
86ab5d5 
This is part one of #12076.

`OrzechProperty R` is a type class stating that `R` satisfies the following property: for any finitely generated `R`-module `M`, any surjective homomorphism `f : N → M` from a submodule `N` of `M` to `M` is injective.

We stated some basic results about `OrzechProperty` and proved that it implies `StrongRankCondition`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: add the definition of OrzechProperty [Merged by Bors] - feat: add the definition of OrzechProperty May 31, 2024
@mathlib-bors mathlib-bors bot closed this May 31, 2024
@mathlib-bors mathlib-bors bot deleted the acmepjz_orzech_def branch May 31, 2024 12:33
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@acmepjz @callesonne
feat: add the definition of OrzechProperty (#13322)
2540b4e 
This is part one of #12076.

`OrzechProperty R` is a type class stating that `R` satisfies the following property: for any finitely generated `R`-module `M`, any surjective homomorphism `f : N → M` from a submodule `N` of `M` to `M` is injective.

We stated some basic results about `OrzechProperty` and proved that it implies `StrongRankCondition`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kbuzzard kbuzzard kbuzzard approved these changes

+1 more reviewer

@AntoineChambert-Loir AntoineChambert-Loir AntoineChambert-Loir 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). t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@acmepjz @jcommelin @AntoineChambert-Loir @kbuzzard