[Merged by Bors] - feat(RingTheory): isotypic API and simple Wedderburn–Artin existence by alreadydone · Pull Request #23963 · leanprover-community/mathlib4

alreadydone · 2025-04-11T23:40:05Z

A replacement of #23583 with more meaningful intermediate results.

Co-authored-by: Edison Xie @Whysoserioushah
Co-authored-by: Jujian Zhang jujian.zhang19@imperial.ac.uk

depends on: [Merged by Bors] - feat: preliminaries for Wedderburn–Artin #24119

Module docstrings are added in #24192, specifically f5b94a2

…variant

github-actions · 2025-04-11T23:41:02Z

PR summary a27e36f668

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.SimpleModule.Basic	1156	1163	+7 (+0.61%)

Import changes for all files

Files	Import difference
24 files `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.CartanMatrix` `Mathlib.Algebra.Lie.Derivation.AdjointAction` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Free` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Ideal` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Algebra.Symmetrized` `Mathlib.RingTheory.Artinian.Algebra` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.Derivation.Lie` `Mathlib.RingTheory.FiniteLength`	5
`Mathlib.RepresentationTheory.Maschke`	6
3 files `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.Topology.Algebra.Module.Simple`	7
`Mathlib.RingTheory.SimpleModule.Isotypic` (new file)	1164
`Mathlib.RingTheory.SimpleModule.WedderburnArtin` (new file)	1264
`Mathlib.RingTheory.SimpleModule.IsAlgClosed` (new file)	1588

Declarations diff

+ IsIsotypic
+ IsIsotypic.isotypicComponent
+ IsIsotypic.linearEquiv_finsupp
+ IsIsotypic.linearEquiv_fun
+ IsIsotypic.of_injective
+ IsIsotypic.of_subsingleton
+ IsIsotypicOfType
+ IsIsotypicOfType.isIsotypic
+ IsIsotypicOfType.isotypicComponent
+ IsIsotypicOfType.linearEquiv_finsupp
+ IsIsotypicOfType.linearEquiv_fun
+ IsIsotypicOfType.of_injective
+ IsIsotypicOfType.of_isSimpleModule
+ IsIsotypicOfType.of_isotypicComponent_eq_top
+ IsIsotypicOfType.of_linearEquiv_type
+ IsIsotypicOfType.of_subsingleton
+ IsSemisimpleModule.exists_linearEquiv_dfinsupp
+ IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp
+ IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed
+ IsSimpleRing.isSemisimpleRing_iff_isArtinianRing
+ IsSimpleRing.tfae
+ LinearEquiv.isIsotypicOfType_iff
+ LinearEquiv.isIsotypicOfType_iff_type
+ LinearEquiv.isIsotypic_iff
+ LinearEquiv.isSemisimpleModule_iff
+ LinearEquiv.isSimpleModule_iff
+ Submodule.IsFullyInvariant
+ Submodule.le_isotypicComponent
+ Submodule.le_linearEquiv_of_le_sSup
+ Submodule.le_linearEquiv_of_sSup_eq_top
+ Submodule.linearEquiv_of_le_sSup
+ Submodule.linearEquiv_of_sSup_eq_top
+ bot_lt_isotypicComponent
+ exists_algEquiv_matrix_divisionRing
+ exists_algEquiv_matrix_divisionRing_finite
+ exists_algEquiv_matrix_end_mulOpposite
+ exists_ringEquiv_matrix_divisionRing
+ exists_ringEquiv_matrix_end_mulOpposite
+ extension_property
+ instance (priority := low) : IsSemisimpleRing R
+ instance [IsSemisimpleModule R S] : IsSemisimpleModule R (isotypicComponent R M S) := by
+ isFullyInvariant_iff_isTwoSided
+ isFullyInvariant_isotypicComponent
+ isIsotypic
+ isIsotypicOfType_submodule_iff
+ isIsotypic_iff_isFullyInvariant_imp_bot_or_top
+ isIsotypic_submodule_iff
+ isSimpleRing_isArtinianRing_iff
+ isotypicComponent
+ isotypicComponent_eq_top_iff
+ linearEquiv_of_ne_zero

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).

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

Mathlib/Algebra/Ring/CentroidHom.lean

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

Whysoserioushah

looks good LGTM

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

Mathlib/Data/Matrix/Basic.lean

Mathlib/Order/Atoms.lean

Mathlib/RingTheory/Jacobson/Ideal.lean

leanprover-community-bot-assistant · 2025-04-27T21:12:14Z

This pull request has conflicts, please merge master and resolve them.

leanprover-community-bot-assistant · 2025-04-28T11:48:46Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-dependent-issues-bot · 2025-05-01T08:04:08Z

This PR/issue depends on:

~~[Merged by Bors] - feat: preliminaries for Wedderburn–Artin #24119~~
By Dependent Issues (🤖). Happy coding!

jcommelin · 2025-05-01T19:05:21Z

Mathlib/RingTheory/SimpleModule/Isotypic.lean

+import Mathlib.RingTheory.SimpleModule.Basic
+
+/-!
+# Isotypic modules and isotypic components


Could you please write a few sentences, e.g. explaining what an isotypic module is? And maybe pointers to the main result(s)?

Sorry, missed the review. Module docstrings are added in the subsequent PR (specifically d870b8b), since both PRs touch these two files.

jcommelin

Modulo a bit of docs on isotypic modules, this looks good to me.

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

jcommelin

Thanks! 🎉

bors merge

@Whysoserioushah

…23963) A replacement of #23583 with more meaningful intermediate results. Co-authored-by: Edison Xie @Whysoserioushah Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)

mathlib-bors · 2025-05-15T15:18:18Z

Pull request successfully merged into master.

Build succeeded:

@Whysoserioushah

…23963) A replacement of #23583 with more meaningful intermediate results. Co-authored-by: Edison Xie @Whysoserioushah Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)

@Whysoserioushah

…eanprover-community#23963) A replacement of leanprover-community#23583 with more meaningful intermediate results. Co-authored-by: Edison Xie @Whysoserioushah Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)

alreadydone added 4 commits April 10, 2025 01:14

feat(RingTheory): Wedderburn-Artin theorem

9234c0e

introduce isotypicComponent; sorry-free isSimpleRing_isArtinianRing_iff

b8acc1e

refactor: introduce IsIsotypicOfType, IsSumIsotypicComponent->IsEndIn…

5ccfee7

…variant

prove existence part of Wedderburn--Artin

984c6aa

alreadydone added the t-algebra Algebra (groups, rings, fields, etc) label Apr 11, 2025

Discard changes to Mathlib/RingTheory/Finiteness/Finsupp.lean

dda420e

Whysoserioushah reviewed Apr 12, 2025

View reviewed changes

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean Outdated Show resolved Hide resolved

alreadydone added 4 commits April 13, 2025 01:14

add NeZero

039aa38

copypasterror

29680b9

AlgEquiv versions

f8c91bc

fixes; remove assert_not_exists Field

1a84384

alreadydone commented Apr 13, 2025

View reviewed changes

Mathlib/Algebra/Ring/CentroidHom.lean Show resolved Hide resolved

Whysoserioushah reviewed Apr 13, 2025

View reviewed changes

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean Outdated Show resolved Hide resolved

alreadydone added 4 commits April 13, 2025 11:30

simpNF

441fd88

docstrings

e1b9568

fix

4adb05f

shake

dfb253e

Whysoserioushah approved these changes Apr 13, 2025

View reviewed changes

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean Outdated Show resolved Hide resolved

Whysoserioushah mentioned this pull request Apr 13, 2025

feat(Mathlib/RingTheory/TwoSidedIdeal/WedderburnArtin): Wedderburn-Artin Theorem #23583

Closed

2 tasks

Whysoserioushah requested review from b-mehta, erdOne, eric-wieser, jcommelin and kbuzzard April 13, 2025 14:50

eric-wieser reviewed Apr 13, 2025

View reviewed changes

Mathlib/Data/Matrix/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 13, 2025

View reviewed changes

Mathlib/Order/Atoms.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 13, 2025

View reviewed changes

Mathlib/RingTheory/Jacobson/Ideal.lean Outdated Show resolved Hide resolved

alreadydone added 2 commits April 13, 2025 17:41

address review

a4ff576

copypasterror

be9e034

Merge branch 'master' into jyxu/WedderburnArtin_simple

c05898e

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 28, 2025

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 Apr 28, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 1, 2025

Merge branch 'master' into jyxu/WedderburnArtin_simple

308d02a

alreadydone 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 1, 2025

alreadydone added 3 commits May 1, 2025 11:25

Discard changes to Mathlib/Algebra/Ring/CentroidHom.lean

fbae1d5

Discard changes to Mathlib/GroupTheory/Perm/DomMulAct.lean

1b2558b

Discard changes to Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean

5d6a07b

jcommelin reviewed May 1, 2025

View reviewed changes

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean Show resolved Hide resolved

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean Show resolved Hide resolved

alreadydone commented May 11, 2025

View reviewed changes

alreadydone added 2 commits May 10, 2025 21:44

decl docstrings

c2d567d

Merge branch 'master' into jyxu/WedderburnArtin_simple

a27e36f

alreadydone requested a review from jcommelin May 15, 2025 09:13

jcommelin reviewed May 15, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label May 15, 2025

mathlib-bors bot changed the title ~~feat(RingTheory): isotypic API and simple Wedderburn–Artin existence~~ [Merged by Bors] - feat(RingTheory): isotypic API and simple Wedderburn–Artin existence May 15, 2025

mathlib-bors bot closed this May 15, 2025

mathlib-bors bot deleted the jyxu/WedderburnArtin_simple branch May 15, 2025 15:18

alreadydone restored the jyxu/WedderburnArtin_simple branch May 15, 2025 15:32

alreadydone deleted the jyxu/WedderburnArtin_simple branch May 15, 2025 15:32

Conversation

alreadydone commented Apr 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary a27e36f668

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Whysoserioushah left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leanprover-community-bot-assistant commented Apr 27, 2025

Uh oh!

leanprover-community-bot-assistant commented Apr 28, 2025

Uh oh!

mathlib4-dependent-issues-bot commented May 1, 2025

Uh oh!

jcommelin May 1, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone May 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented May 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

alreadydone commented Apr 11, 2025 •

edited

Loading

github-actions bot commented Apr 11, 2025 •

edited

Loading

alreadydone May 11, 2025 •

edited

Loading