[Merged by Bors] - feat(RingTheory): semisimple Wedderburn–Artin existence#24192
[Merged by Bors] - feat(RingTheory): semisimple Wedderburn–Artin existence#24192alreadydone wants to merge 42 commits intomasterfrom
Conversation
PR summary 25b3be17c7
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.SimpleModule.Isotypic | 1192 | 1195 | +3 (+0.25%) |
| Mathlib.RingTheory.SimpleModule.WedderburnArtin | 1306 | 1308 | +2 (+0.15%) |
| Mathlib.Algebra.Algebra.Pi | 727 | 728 | +1 (+0.14%) |
| Mathlib.RingTheory.SimpleModule.IsAlgClosed | 1627 | 1629 | +2 (+0.12%) |
Import changes for all files
| Files | Import difference |
|---|---|
25 filesMathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.StarAlgHom Mathlib.LinearAlgebra.StdBasis Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Projective Mathlib.RingTheory.OrzechProperty Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.LocallyConvex Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.UniformSpace.ProdApproximation |
1 |
Mathlib.RingTheory.SimpleModule.IsAlgClosed Mathlib.RingTheory.SimpleModule.WedderburnArtin |
2 |
Mathlib.RingTheory.SimpleModule.Isotypic |
3 |
Declarations diff
+ GaloisCoinsertion.setIsotypicComponents
+ IsIsotypic.isotypicComponents
+ IsIsotypic.submodule_linearEquiv_fun
+ IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed
+ LinearEquiv.isotypicComponent_eq
+ LinearMap.le_comap_isotypicComponent
+ OrderIso.setIsotypicComponents
+ Submodule.IsFullyInvariant.isotypicComponent
+ Submodule.IsFullyInvariant.of_mem_isotypicComponents
+ Submodule.map_le_isotypicComponent
+ bot_lt_isotypicComponents
+ bot_mem
+ coe_iInf
+ coe_iSup
+ endAlgEquiv
+ endRingEquiv
+ eq_isotypicComponent_iff
+ eq_isotypicComponent_of_le
+ exists_algEquiv_pi_matrix_divisionRing
+ exists_algEquiv_pi_matrix_divisionRing_finite
+ exists_algEquiv_pi_matrix_end_mulOpposite
+ exists_end_algEquiv
+ exists_end_ringEquiv
+ exists_ringEquiv_pi_matrix_divisionRing
+ exists_ringEquiv_pi_matrix_end_mulOpposite
+ fullyInvariantSubmodule
+ iSupIndep.algEquiv
+ iSupIndep.linearEquiv
+ iSupIndep.linearEquiv_symm_apply
+ iSupIndep.ringEquiv
+ instance (c : isotypicComponents R M) : IsSemisimpleModule R c := by
+ instance (c : isotypicComponents R M) : Nontrivial c
+ instance [IsNoetherian R M] : Finite (isotypicComponents R M)
+ isFullyInvariant_iff_le_imp_isotypicComponent_le
+ isFullyInvariant_iff_sSup_isotypicComponents
+ isotypicComponents
+ le_isotypicComponent_iff
+ mem_fullyInvariantSubmodule_iff
+ mem_isotypicComponents_iff
+ sSupIndep_isotypicComponents
+ sSup_isotypicComponents
+ top_mem
++ piMulOpposite
- isFullyInvariant_isotypicComponent
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).
|
This pull request has conflicts, please merge |
|
This pull request has conflicts, please merge |
| theorem exists_end_algEquiv : | ||
| ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ), | ||
| (∀ i, IsSimpleModule R (S i)) ∧ (∀ i, NeZero (d i)) ∧ | ||
| Nonempty (End R M ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (End R (S i))) := by |
There was a problem hiding this comment.
Is it common practice to use exists in the name, but Nonempty in the type?
Idem dito below
There was a problem hiding this comment.
Technically Exists does appear as the head symbol in all these statements, including all existing statements above; they refer to the existence of dimensions of the matrices, simple modules, and division rings/algebras which are not pre-determined. I think it's reasonable to expect people to search exists for these theorems, so using exists doesn't make these harder to discover and we can continue to use exists.
There was a problem hiding this comment.
Good point, I agree!
bors merge
|
Other than one minor comment about naming, this looks good to me. bors d+ |
|
✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Pull request successfully merged into master. Build succeeded: |
Uh oh!
There was an error while loading. Please reload this page.