[Merged by Bors] - feat: Prerequisites for Hopkins–Levitzki theorem#21544
Closed
alreadydone wants to merge 22 commits intomasterfrom
Closed
[Merged by Bors] - feat: Prerequisites for Hopkins–Levitzki theorem#21544alreadydone wants to merge 22 commits intomasterfrom
alreadydone wants to merge 22 commits intomasterfrom
Conversation
PR summary e471f90fff
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Algebra.Module.Simple | 1310 | 1214 | -96 (-7.33%) |
| Mathlib.RepresentationTheory.Maschke | 1187 | 1109 | -78 (-6.57%) |
| Mathlib.RingTheory.FiniteLength | 1221 | 1171 | -50 (-4.10%) |
| Mathlib.RingTheory.Artinian.Instances | 1278 | 1239 | -39 (-3.05%) |
| Mathlib.Algebra.Module.Torsion | 1226 | 1240 | +14 (+1.14%) |
| Mathlib.LinearAlgebra.Semisimple | 1513 | 1509 | -4 (-0.26%) |
| Mathlib.Algebra.Module.PID | 1716 | 1712 | -4 (-0.23%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.SimpleModule |
-1183 |
Mathlib.Topology.Algebra.Module.Simple |
-96 |
Mathlib.RepresentationTheory.Maschke |
-78 |
Mathlib.RingTheory.FiniteLength |
-50 |
Mathlib.RingTheory.Artinian.Instances |
-39 |
6 filesMathlib.Algebra.Module.PID Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.LinearAlgebra.Semisimple Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.MulChar.Duality |
-4 |
Mathlib.LinearAlgebra.JordanChevalley |
-1 |
9 filesMathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.Locus |
7 |
53 filesMathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.FieldTheory.JacobsonNoether Mathlib.LinearAlgebra.Reflection Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Extension Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Generators Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Presentation Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Pi |
9 |
4 filesMathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.Regular.RegularSequence |
10 |
Mathlib.RingTheory.AdicCompletion.Exactness |
11 |
Mathlib.RingTheory.Regular.IsSMulRegular |
12 |
4 filesMathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.Module.Torsion Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.RingTheory.AdicCompletion.Functoriality |
14 |
Mathlib.RingTheory.SimpleModule.Basic |
1087 |
Mathlib.RingTheory.SimpleModule.Rank (new file) |
1184 |
Declarations diff
+ Ideal.isMaximal_iff_isPrime
+ Ideal.isMaximal_of_isPrime
+ Ideal.mem_minimalPrimes_iff_isPrime
+ Ideal.mem_minimalPrimes_of_krullDimLE_zero
+ IsCoatom.codisjoint_of_ne
+ IsNoetherianRing.of_finite
+ IsSemisimpleModule.isCoatomic_submodule
+ IsTorsionBySet.isSemisimpleModule_iff
+ LinearMap.isNoetherian_iff_of_bijective
+ Module.annihilator_eq_top_iff
+ Ring.krullDimLE_one_iff_of_noZeroDivisors
+ RingEquiv.isSemisimpleRing_iff
+ comap_map_sup_of_comap_le
+ discreteTopology_iff_finite_and_krullDimLE_zero
+ exists_inf_eq_iInf
+ exists_inf_le
+ exists_sup_eq_iSup
+ exists_sup_ge
+ iSup_range_lsingle
+ injective_pi_lapply
+ instance (priority := 100) (I : Ideal R) [I.IsPrime] [Ring.KrullDimLE 0 R] : I.IsMaximal
+ instance : Ring.KrullDimLE 0 R := .mk₀ fun _ _ ↦ inferInstance
+ instance [Module.Finite R M] : IsCoatomic (Submodule R M)
+ instance [Ring.KrullDimLE 0 R] : Ring.KrullDimLE 1 R := .mono zero_le_one _
+ instance [Subsingleton R] : Ring.KrullDimLE 0 R := ⟨krullDim_eq_bot.trans_le bot_le⟩
+ instance {ι} (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
+ instance {ι} [Finite ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
+ isCoatom_comap_iff
+ isCoatom_comap_or_eq_top
+ isCoatom_map_of_ker_le
+ isCoprime_of_isMaximal
+ isSemisimpleModule_iff_exists_linearEquiv_dfinsupp
+ le_annihilator_iff
+ le_map_of_comap_le_of_surjective
+ lsum_lsingle
+ lt_map_of_comap_lt_of_surjective
+ map_iInf_of_ker_le
+ of_injective
+ of_surjective
+ pi_univ_bot
+ proj_surjective
- IsSemisimpleRing.isCoatomic_submodule
- Ring.krullDimLE_one_iff_of_isDomain
- instance (priority := 100) Ideal.isMaximal_of_isPrime [Ring.KrullDimLE 0 R]
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
1 task
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit be38aaf. |
3 files, Instructions +1.0⬝10⁹
|
jcommelin
reviewed
Feb 7, 2025
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 7, 2025
Co-authored-by: Johan Commelin <johan@commelin.net>
Contributor
|
Build failed:
|
Contributor
Author
|
The failure is due to this new test just merged into mathlib, which means that even though I removed the simp attribute I still need to keep this test working, which I try to do by lowering priority. It might also help to change the argument order of Ideal.isMaximal_of_isPrime like in #21449. (Update: a different fix is implemented.) |
alreadydone
commented
Feb 7, 2025
Member
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 7, 2025
**RingTheory/HopkinsLevitzki.lean** requires: + **Order/Atoms.lean**, **RingTheory/Ideal/Operations.lean**: show two distinct maximal ideals are coprime (comaximal). + **RingTheory/Ideal/Maps.lean**: add two lemmas about annihilators. + **Algebra/Module/Torsion.lean**: add a lemma about being a semisimple module over a quotient ring. + **RingTheory/KrullDimension/Basic.lean**: add lemmas about zero-dimensional rings. + **RingTheory/Spectrum/Prime/Topology.lean**: switch to `Ring.KrullDimLE`. **RingTheory/Jacobson/Radical.lean** requires: + **Algebra/Module/Submodule/Map.lean** and **LinearAlgebra/Span/Basic.lean**: Lemmas used to show functoriality of Jacobson radical of modules (`le_comap_jacobson`). **RingTheory/SimpleModule.lean**: split out a single lemma that requires `Module.finrank` to reduce imports: **SimpleModule.lean** is renamed **SimpleModule/Basic.lean**, and the lemma is moved into **SimpleModule/Rank.lean**. + **LinearAlgebra/DFinsupp.lean**: add lemmas to show a direct sum of semisimple modules is semisimple. **RingTheory/Artinian/Module.lean** requires: + **RingTheory/Artinian/Instances.lean**: move an instance to Artinian/Module, which now imports SimpleModule. + **Data/Finset/Lattice/Fold.lean**: add lemmas used to golf [IsArtinianRing.setOf_isMaximal_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Artinian/Module.html#IsArtinianRing.setOf_isMaximal_finite) and in the proof of that an Artinian ring is semiprimary. Co-authored-by: Johan Commelin <johan@commelin.net>
Contributor
|
Build failed (retrying...): |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 7, 2025
**RingTheory/HopkinsLevitzki.lean** requires: + **Order/Atoms.lean**, **RingTheory/Ideal/Operations.lean**: show two distinct maximal ideals are coprime (comaximal). + **RingTheory/Ideal/Maps.lean**: add two lemmas about annihilators. + **Algebra/Module/Torsion.lean**: add a lemma about being a semisimple module over a quotient ring. + **RingTheory/KrullDimension/Basic.lean**: add lemmas about zero-dimensional rings. + **RingTheory/Spectrum/Prime/Topology.lean**: switch to `Ring.KrullDimLE`. **RingTheory/Jacobson/Radical.lean** requires: + **Algebra/Module/Submodule/Map.lean** and **LinearAlgebra/Span/Basic.lean**: Lemmas used to show functoriality of Jacobson radical of modules (`le_comap_jacobson`). **RingTheory/SimpleModule.lean**: split out a single lemma that requires `Module.finrank` to reduce imports: **SimpleModule.lean** is renamed **SimpleModule/Basic.lean**, and the lemma is moved into **SimpleModule/Rank.lean**. + **LinearAlgebra/DFinsupp.lean**: add lemmas to show a direct sum of semisimple modules is semisimple. **RingTheory/Artinian/Module.lean** requires: + **RingTheory/Artinian/Instances.lean**: move an instance to Artinian/Module, which now imports SimpleModule. + **Data/Finset/Lattice/Fold.lean**: add lemmas used to golf [IsArtinianRing.setOf_isMaximal_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Artinian/Module.html#IsArtinianRing.setOf_isMaximal_finite) and in the proof of that an Artinian ring is semiprimary. Co-authored-by: Johan Commelin <johan@commelin.net>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
RingTheory/HopkinsLevitzki.lean requires:
Ring.KrullDimLE.RingTheory/Jacobson/Radical.lean requires:
le_comap_jacobson).RingTheory/SimpleModule.lean: split out a single lemma that requires
Module.finrankto reduce imports: SimpleModule.lean is renamed SimpleModule/Basic.lean, and the lemma is moved into SimpleModule/Rank.lean.RingTheory/Artinian/Module.lean requires: