Skip to content

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

Closed
chrisflav wants to merge 10 commits into
masterfrom
chrisflav/presentation
Closed

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

Conversation

@chrisflav

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

Copy link
Copy Markdown
Member

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

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

Copy link
Copy Markdown

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
Comment thread Mathlib/RingTheory/Localization/Away/Basic.lean Outdated
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/MvPolynomial/Localization.lean Outdated
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
erdOne
erdOne reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Localization/Away/Basic.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
@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
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
@chrisflav

chrisflav commented Jun 30, 2024

Copy link
Copy Markdown
Member Author

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

MichaelStollBayreuth commented Jun 30, 2024

Copy link
Copy Markdown
Contributor

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

kbuzzard commented Jun 30, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

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

chrisflav commented Jun 30, 2024

Copy link
Copy Markdown
Member Author

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
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
Comment thread Mathlib/RingTheory/Presentation.lean
Comment thread Mathlib/RingTheory/Generators.lean Outdated
Comment thread Mathlib/RingTheory/Generators.lean
@chrisflav chrisflav mentioned this pull request Jun 30, 2024
Closed
erdOne
erdOne reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Presentation.lean
erdOne
erdOne reviewed Jun 30, 2024
View reviewed changes
Comment thread Mathlib/RingTheory/Presentation.lean Outdated
@erdOne

erdOne commented Jun 30, 2024

Copy link
Copy Markdown
Member

LGTM. What does @MichaelStollBayreuth think?

MichaelStollBayreuth
MichaelStollBayreuth approved these changes Jun 30, 2024
View reviewed changes

@MichaelStollBayreuth MichaelStollBayreuth left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM!

@MichaelStollBayreuth

MichaelStollBayreuth commented Jun 30, 2024

Copy link
Copy Markdown
Contributor

maintainer merge

@github-actions

github-actions Bot commented Jun 30, 2024

Copy link
Copy Markdown

🚀 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

riccardobrasca commented Jul 1, 2024

Copy link
Copy Markdown
Member

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

chrisflav commented Jul 1, 2024

Copy link
Copy Markdown
Member Author

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 <[email protected]>
@mathlib-bors

mathlib-bors Bot commented Jul 1, 2024

Copy link
Copy Markdown
Contributor

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 <[email protected]>
@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