Skip to content

[Merged by Bors] - feat(RingTheory): presentations of algebras#14271

Closed
chrisflav wants to merge 10 commits intomasterfrom
chrisflav/presentation
Closed

[Merged by Bors] - feat(RingTheory): presentations of algebras#14271
chrisflav wants to merge 10 commits intomasterfrom
chrisflav/presentation

Conversation

@chrisflav
Copy link
Copy Markdown
Member

@chrisflav chrisflav commented Jun 29, 2024 •
edited by erdOne
Loading

Adds basic API for presentations of algebras and constructors for localization and base change.

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Co-authored-by: Andrew Yang @erdOne
Co-authored-by: Jung Tao Cheng @rontaucheng

Open in Gitpod

@chrisflav chrisflav added awaiting-review 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 labels Jun 29, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary d93929f0eb

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.RingTheory.MvPolynomial.Localization 989 1023 +34 (+3.44%)
Mathlib.RingTheory.Generators 1152 1155 +3 (+0.26%)

Declarations diff

+ Algebra.Presentation
+ IsFinite
+ aeval_val_relation
+ auxHom
+ auxInv
+ dimension
+ finitePresentation_of_isFinite
+ ideal_fg_of_isFinite
+ instance [P.IsFinite] : FinitePresentation R P.Quotient
+ ker_eq_ker_aeval_val
+ localizationAway_dimension_zero
+ localizationAway_isFinite
+ mk'_pow
+ mvPolynomialQuotientEquiv
+ mvPolynomialQuotientEquiv_apply
+ quotientEquiv
+ quotientEquiv_mk
+ quotientEquiv_symm
+ sec
+ sec_spec
++ baseChange
++ localizationAway

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>

MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
erdOne
erdOne reviewed Jun 30, 2024
View reviewed changes
@erdOne erdOne added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 30, 2024
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
@chrisflav
Copy link
Copy Markdown
Member Author

chrisflav commented Jun 30, 2024

Thanks for the quick reviews!

@chrisflav chrisflav added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 30, 2024
@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

MichaelStollBayreuth commented Jun 30, 2024

A question for native English speakers: Which is correct?

  • "A R-algebra"
  • "An R-algebra"

My gut feeling says it's the second one (since it corresponds to what I would say when reading it), but I wouldn't want to claim I know all the rules.

@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jun 30, 2024 •
edited
Loading

A question for native English speakers: Which is correct?

  • "A R-algebra"
  • "An R-algebra"

My gut feeling says it's the second one (since it corresponds to what I would say when reading it), but I wouldn't want to claim I know all the rules.

Definitely "an R-algebra". Indeed the rule is "write what you would say", and what you say depends on the sound not the actual letter (so e.g. "a eucalyptus tree" as the word is pronounced "Yucaliptus")

@chrisflav
Copy link
Copy Markdown
Member Author

chrisflav commented Jun 30, 2024

A question for native English speakers: Which is correct?

  • "A R-algebra"
  • "An R-algebra"

My gut feeling says it's the second one (since it corresponds to what I would say when reading it), but I wouldn't want to claim I know all the rules.

Definitely "an R-algebra". Indeed the rule is "write what you would say", and what you say depends on the sound not the actual letter (so e.g. "a eucalyptus tree" as the word is pronounced "Yucaliptus")

Fixed.

erdOne
erdOne reviewed Jun 30, 2024
View reviewed changes
@chrisflav chrisflav mentioned this pull request Jun 30, 2024
Closed
erdOne
erdOne reviewed Jun 30, 2024
View reviewed changes
@chrisflav @erdOne
Update Mathlib/RingTheory/Presentation.lean
f63df19 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
erdOne
erdOne reviewed Jun 30, 2024
View reviewed changes
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 30, 2024

LGTM. What does @MichaelStollBayreuth think?

MichaelStollBayreuth
MichaelStollBayreuth approved these changes Jun 30, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@MichaelStollBayreuth MichaelStollBayreuth left a comment

Choose a reason for hiding this comment

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

LGTM!

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

MichaelStollBayreuth commented Jun 30, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 30, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 30, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jul 1, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 1, 2024
@chrisflav
Copy link
Copy Markdown
Member Author

chrisflav commented Jul 1, 2024

Thanks for all the reviews!

mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024
@chrisflav
feat(RingTheory): presentations of algebras (#14271)
58877de 
Adds basic API for presentations of algebras and constructors for localization and base change.

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Co-authored-by: Andrew Yang @erdOne
Co-authored-by: Jung Tao Cheng @rontaucheng 



Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory): presentations of algebras [Merged by Bors] - feat(RingTheory): presentations of algebras Jul 1, 2024
@mathlib-bors mathlib-bors bot closed this Jul 1, 2024
@mathlib-bors mathlib-bors bot deleted the chrisflav/presentation branch July 1, 2024 09:41
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@chrisflav @dagurtomas
feat(RingTheory): presentations of algebras (#14271)
9f744ba 
Adds basic API for presentations of algebras and constructors for localization and base change.

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Co-authored-by: Andrew Yang @erdOne
Co-authored-by: Jung Tao Cheng @rontaucheng 



Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
@chrisflav chrisflav mentioned this pull request Jul 24, 2024
Closed
3 tasks
@adomani adomani mentioned this pull request Aug 1, 2024
Open
@chrisflav chrisflav mentioned this pull request Sep 17, 2024
Open
5 tasks
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

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth approved these changes

Assignees

No one assigned

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) workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@chrisflav @MichaelStollBayreuth @kbuzzard @erdOne @riccardobrasca