[Merged by Bors] - feat(LinearAlgebra): Symmetric Algebra by Raph-DG · Pull Request #21539 · leanprover-community/mathlib4

Raph-DG · 2025-02-07T10:30:30Z

Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module.

Co-authored-by: Zhixuan Dai 22300180006@m.fudan.edu.cn
Co-authored-by: Zhenyan Fu fuzhenyan@mail.dlut.edu.cn
Co-authored-by: Yiming Fu fakegreenall@foxmail.com
Co-authored-by: Wang Jingting wangjt2020@163.com

github-actions · 2025-02-07T10:31:30Z

PR summary 74f4ad6ae9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.SymmetricAlgebra.Basic` (new file)	1023
`Mathlib.LinearAlgebra.SymmetricAlgebra.Basis` (new file)	1329

Declarations diff

+ SymmetricAlgebra
+ TensorAlgebra.SymRel
+ _root_.Basis.symmetricAlgebra
+ algHom
+ algHom_ext
+ algHom_surjective
+ algebraMapInv
+ algebraMap_eq_one_iff
+ algebraMap_eq_zero_iff
+ algebraMap_inj
+ algebraMap_leftInverse
+ equivMvPolynomial
+ equivMvPolynomial_symm_X
+ equivMvPolynomial_ι_apply
+ induction
+ instIsDomain
+ instModuleFree
+ instNoZeroDivisors
+ instance (R M) [CommRing R] [AddCommMonoid M] [Module R M] : CommRing (SymmetricAlgebra R M)
+ instance : CommSemiring (SymmetricAlgebra R M)
+ instance [Nontrivial R] : Nontrivial (SymmetricAlgebra R M)
+ lift
+ lift_comp_ι
+ lift_ι
+ lift_ι_apply
+ rank_eq
+ ι

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

I guess it's probably customary to write the names of Chinese people with first names coming first(?)

slight changes about indentation and other stuff

Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean

eric-wieser · 2025-05-10T22:12:56Z

I copied across the algebraMapInv stuff from TensorAlgebra so that the Basis.lean file can be exactly in parity with the TensorAlgebra version, and tweaked some sectioning to make them match.

maintainer merge

github-actions · 2025-05-10T22:13:14Z

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

github-actions · 2025-05-10T22:14:09Z

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean

kbuzzard

Thanks!

bors d+

mathlib-bors · 2025-05-10T22:46:54Z

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

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Raph-DG · 2025-05-11T13:00:37Z

bors r+

Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module. Co-authored-by: Zhixuan Dai <22300180006@m.fudan.edu.cn> Co-authored-by: Zhenyan Fu <fuzhenyan@mail.dlut.edu.cn> Co-authored-by: Yiming Fu <fakegreenall@foxmail.com> Co-authored-by: Wang Jingting <wangjt2020@163.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-05-11T13:01:59Z

Build failed:

Build

Raph-DG · 2025-05-11T14:01:31Z

bors r+

Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module. Co-authored-by: Zhixuan Dai <22300180006@m.fudan.edu.cn> Co-authored-by: Zhenyan Fu <fuzhenyan@mail.dlut.edu.cn> Co-authored-by: Yiming Fu <fakegreenall@foxmail.com> Co-authored-by: Wang Jingting <wangjt2020@163.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-05-11T14:08:04Z

Pull request successfully merged into master.

Build succeeded:

Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module. Co-authored-by: Zhixuan Dai <22300180006@m.fudan.edu.cn> Co-authored-by: Zhenyan Fu <fuzhenyan@mail.dlut.edu.cn> Co-authored-by: Yiming Fu <fakegreenall@foxmail.com> Co-authored-by: Wang Jingting <wangjt2020@163.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Raph-DG added 12 commits January 28, 2025 10:30

Added file with basic lemmas for symmetric algebras

aa31f8b

Fixing build issues

58ae740

Added additional documentation

ee784f5

Added more documentation

e896ab4

Fixed warning

f61df42

Merge branch 'master' into Raph-DG-SymmetricAlgebra

1c433f9

Added authors, hopefully fixed build errors

75bb2dd

Fixed imports

6dec797

Merge branch 'master' into Raph-DG-SymmetricAlgebra

419ef08

restore lake-manifest.json

ee366cc

Added some have statements used for rewriting as simp lemmas

2e24541

Fixed simp issues

53e058f

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 7, 2025

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Feb 7, 2025

xyzw12345 added 2 commits February 10, 2025 18:52

Update Basic.lean

252023f

I guess it's probably customary to write the names of Chinese people with first names coming first(?)

Update Basic.lean

48decd7

slight changes about indentation and other stuff

Raph-DG requested a review from jcommelin February 10, 2025 16:08

ADedecker reviewed Feb 20, 2025

View reviewed changes

Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean Outdated Show resolved Hide resolved

xyzw12345 mentioned this pull request Feb 25, 2025

feat(RingTheory/GradedAlgebra): homogeneous relation #22279

Closed

1 task

xyzw12345 added 6 commits March 13, 2025 21:25

Merge branch 'master' into Raph-DG-SymmetricAlgebra

f3c7983

Refactoring in progress

60ec781

added theorems to prove

ba6aa7f

prove some theorems

b5a21e4

finished proof

b11d3b7

update docstring

c6472fe

xyzw12345 requested review from ADedecker and chrisflav March 15, 2025 06:20

xyzw12345 added 2 commits March 15, 2025 14:22

changed from CommRing to CommSemiring

12f916c

update docstring

f568216

xyzw12345 added 2 commits May 6, 2025 09:52

update docstring

62709a4

update docstring

40c4a01

xyzw12345 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 6, 2025

xyzw12345 requested a review from eric-wieser May 6, 2025 01:53

increase parity with TensorAlgebra

08f4c94

kbuzzard reviewed May 10, 2025

View reviewed changes

Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean Outdated Show resolved Hide resolved

kbuzzard approved these changes May 10, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 10, 2025

xyzw12345 and others added 2 commits May 11, 2025 13:21

Update Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean

5b750f0

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

fix docstring

05e391f

xyzw12345 and others added 3 commits May 11, 2025 21:14

Merge branch 'master' into Raph-DG-SymmetricAlgebra

b5bf459

Update Basic.lean

4cb04b5

prune import

74f4ad6

mathlib-bors bot changed the title ~~feat(LinearAlgebra): Symmetric Algebra~~ [Merged by Bors] - feat(LinearAlgebra): Symmetric Algebra May 11, 2025

mathlib-bors bot closed this May 11, 2025

mathlib-bors bot deleted the Raph-DG-SymmetricAlgebra branch May 11, 2025 14:08

alreadydone mentioned this pull request Feb 9, 2026

feat(RingTheory/GradedAlgebra): homogeneous relation #27307

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(LinearAlgebra): Symmetric Algebra#21539

[Merged by Bors] - feat(LinearAlgebra): Symmetric Algebra#21539
Raph-DG wants to merge 84 commits intomasterfrom
Raph-DG-SymmetricAlgebra

Raph-DG commented Feb 7, 2025 •

edited by YaelDillies

Loading

Uh oh!

github-actions bot commented Feb 7, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

eric-wieser commented May 10, 2025 •

edited

Loading

Uh oh!

github-actions bot commented May 10, 2025

Uh oh!

github-actions bot commented May 10, 2025

Uh oh!

Uh oh!

kbuzzard left a comment

Uh oh!

mathlib-bors bot commented May 10, 2025

Uh oh!

Raph-DG commented May 11, 2025

Uh oh!

mathlib-bors bot commented May 11, 2025

Uh oh!

Raph-DG commented May 11, 2025

Uh oh!

mathlib-bors bot commented May 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

Raph-DG commented Feb 7, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 74f4ad6ae9

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

eric-wieser commented May 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented May 10, 2025

Uh oh!

github-actions bot commented May 10, 2025

Uh oh!

Uh oh!

kbuzzard left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented May 10, 2025

Uh oh!

Raph-DG commented May 11, 2025

Uh oh!

mathlib-bors bot commented May 11, 2025

Uh oh!

Raph-DG commented May 11, 2025

Uh oh!

mathlib-bors bot commented May 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Raph-DG commented Feb 7, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Feb 7, 2025 •

edited

Loading

eric-wieser commented May 10, 2025 •

edited

Loading