[Merged by Bors] - feat(Algebra): more on `OrthogonalIdempotents` #18195

Whysoserioushah · 2024-10-24T18:17:41Z

Co-authored-by : @jjaassoonn

github-actions · 2024-10-24T18:18:29Z

PR summary 63dcdd9437

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.DirectSum.Idempotents` (new file)	1092

Declarations diff

+ completeOrthogonalIdempotents_idempotent
+ decompose_eq_mul_idempotent
+ idempotent
+ isIdempotentElem_idempotent

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

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Mathlib/RingTheory/Idempotents.lean

erdOne

Wait I just noticed I deleted a review by Moritz on accident. I'm very sorry about that. This is the reconstructed review according to my mailbox.

Mathlib/RingTheory/Idempotents.lean

Co-authored-by: Andrew Yang <[email protected]>

…ts' into Primitive-Idempotents

Mathlib/Algebra/DirectSum/Decomposition.lean

Mathlib/RingTheory/Idempotents.lean

Mathlib/Algebra/DirectSum/Idempotents.lean

Co-authored-by: Andrew Yang <[email protected]>

Mathlib/Algebra/DirectSum/Idempotents.lean

Co-authored-by: Andrew Yang <[email protected]>

Mathlib/Algebra/DirectSum/Decomposition.lean

erdOne

The PR looks good to me aside from some docstrings that I couldn't fully parse nor improve on.

But I think I have requested too many alterations to comfortably maintainer merge this and I'll wait for a third opinion.

Mathlib/RingTheory/Idempotents.lean

Mathlib/Algebra/DirectSum/Idempotents.lean

Co-authored-by: Kevin Buzzard <[email protected]>

Mathlib/Algebra/DirectSum/Idempotents.lean

kbuzzard · 2025-01-04T18:39:30Z

Thanks a lot!

bors d+

mathlib-bors · 2025-01-04T18:39:32Z

✌️ Whysoserioushah 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 <[email protected]>

Whysoserioushah · 2025-01-04T18:50:06Z

bors r+

@jjaassoonn

Co-authored-by : @jjaassoonn Co-authored-by: Whysoserioushah <[email protected]>

mathlib-bors · 2025-01-04T19:04:20Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (133 commits) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) feat(Topology/Group): Lemmas about profinite group (#20282) feat: the empty set is a topological basis iff the space is empty (#20441) chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242) chore: `inherit_doc`s for notations (#20376) chore: split AEEqOfIntegral into two files, one for each integral type (#20405) chore: split Kernel/MeasurableIntegral (#20427) feat(MeasureTheory/Group/Measure): add ContinuousMulEquiv.isHaarMeasure_map (#20469) fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic (#20422) feat(Probability/Moments): add lemmas about moment generating functions (#19886) feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954) chore: bump toolchain to v4.15.0 (#20461) chore: update Mathlib dependencies 2025-01-04 (#20463) fix: make `Prod` projection delaborators respond to options, add option to disable (#20455) chore(Algebra): Improve attribute generation (#20451) feat(Polynomial): `(C a * p).degree = p.degree` if `a * p.leadingCoeff ≠ 0` (#20446) feat: add `ENNReal.finStronglyMeasurable_of_measurable` (#20404) doc(Algebra/Lie/Weights/Basic): fix typo (#20450) chore(1000): remove `identifiers` (#20445) feat: add sumPiEquivProdPi and piUnique (#20195) feat: add fst_compProd_apply (#20429) chore: use unsigned measures for Lebesgue decomposition (#20400) feat: Two lemmas on divisibility and coprimality of `expand` (#20143) ...

* origin/master: (189 commits) chore(Algebra): make more names consistent (#20449) feat: Polynomial FLT (#18882) feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457) fix: linkfix in 100.yaml (#20517) feat(1000): fill in more entries (#20470) feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769) feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462) feat(RingTheory): classification of etale algebras over fields (#20324) fix: Allow multiple builds on staging branch (#20515) feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337) chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514) refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474) feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544) chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) feat(CategoryTheory): products in the category of Ind-objects (#20507) chore: remove >9 month old deprecations (#20505) chore(FieldTheory/Galois): small cleanup (#20217) chore(LinearIndependent): generalize to semirings (#20480) chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) chore: replace `aesop` with `simp` where possible (#20483) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) ...

alreadydone · 2025-01-06T22:06:07Z

Mathlib/Algebra/DirectSum/Idempotents.lean

+theorem completeOrthogonalIdempotents_idempotent [Fintype I]:
+    CompleteOrthogonalIdempotents fun i ↦ idempotent V i where


You might be interested in reviewing #20531, which goes the other way around.
I think this is generalizable to semirings too :)

primitiveidempotents

c15ba2c

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 Oct 24, 2024

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 24, 2024

Whysoserioushah and others added 5 commits October 24, 2024 19:25

fix lint

62e0a53

Update Mathlib/RingTheory/Idempotents.lean

d18845b

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/RingTheory/Idempotents.lean

45bfe19

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/RingTheory/Idempotents.lean

0e5fb1f

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/RingTheory/Idempotents.lean

b34a35f

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

erdOne self-assigned this Oct 24, 2024

Whysoserioushah requested a review from kbuzzard October 24, 2024 18:30

changename

aec5382

jjaassoonn requested changes Oct 24, 2024

View reviewed changes

Mathlib/RingTheory/Idempotents.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Idempotents.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Idempotents.lean Outdated Show resolved Hide resolved

jjaassoonn reviewed Oct 24, 2024

View reviewed changes

Mathlib/RingTheory/Idempotents.lean Outdated Show resolved Hide resolved

jjaassoonn reviewed Oct 24, 2024

View reviewed changes

Mathlib/RingTheory/Idempotents.lean Outdated Show resolved Hide resolved

leanprover-community deleted a comment from mo271 Oct 24, 2024

erdOne reviewed Oct 24, 2024

View reviewed changes

Mathlib/RingTheory/Idempotents.lean Outdated Show resolved Hide resolved

erdOne reviewed Oct 24, 2024

View reviewed changes

Mathlib/RingTheory/Idempotents.lean Outdated Show resolved Hide resolved

Whysoserioushah and others added 4 commits October 25, 2024 14:45

Update Mathlib/RingTheory/Idempotents.lean

29891b3

Co-authored-by: Andrew Yang <[email protected]>

fix

6773092

Merge remote-tracking branch 'refs/remotes/origin/Primitive-Idempoten…

cafd7ef

…ts' into Primitive-Idempotents

apply suggestions

813f64d

Whysoserioushah requested a review from jjaassoonn October 25, 2024 14:10

advice

5d0b3e9

kbuzzard reviewed Oct 25, 2024

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 29, 2024

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 Nov 25, 2024

Whysoserioushah removed the awaiting-author A reviewer has asked the author a question or requested changes label Dec 30, 2024

merge1

c93b2a8

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 30, 2024

Whysoserioushah added 2 commits January 4, 2025 20:37

Merge remote-tracking branch 'origin/master' into Primitive-Idempotents

1c535f0

andrew's review 2

200c980

Whysoserioushah removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 4, 2025

erdOne reviewed Jan 4, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Idempotents.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/DirectSum/Idempotents.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/DirectSum/Idempotents.lean Outdated Show resolved Hide resolved

Whysoserioushah and others added 3 commits January 4, 2025 21:44

Update Mathlib/Algebra/DirectSum/Idempotents.lean

0d1def1

Co-authored-by: Andrew Yang <[email protected]>

Update Mathlib/Algebra/DirectSum/Idempotents.lean

b16981e

Co-authored-by: Andrew Yang <[email protected]>

Update Mathlib/Algebra/DirectSum/Idempotents.lean

6d8a634

Co-authored-by: Andrew Yang <[email protected]>

erdOne reviewed Jan 4, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Idempotents.lean Outdated Show resolved Hide resolved

Whysoserioushah and others added 2 commits January 4, 2025 21:49

Update Mathlib/Algebra/DirectSum/Idempotents.lean

1ef9bf8

Co-authored-by: Andrew Yang <[email protected]>

documentation

9b2c2ac

erdOne reviewed Jan 4, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Decomposition.lean Outdated Show resolved Hide resolved

delete

d7c89c3

erdOne approved these changes Jan 4, 2025

View reviewed changes

kbuzzard reviewed Jan 4, 2025

View reviewed changes

Mathlib/RingTheory/Idempotents.lean Show resolved Hide resolved

Mathlib/Algebra/DirectSum/Idempotents.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/DirectSum/Idempotents.lean Outdated Show resolved Hide resolved

Whysoserioushah and others added 2 commits January 5, 2025 02:32

Update Mathlib/Algebra/DirectSum/Idempotents.lean

8a5a282

Co-authored-by: Kevin Buzzard <[email protected]>

Update Mathlib/Algebra/DirectSum/Idempotents.lean

89c2104

Co-authored-by: Kevin Buzzard <[email protected]>

kbuzzard reviewed Jan 4, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Idempotents.lean Show resolved Hide resolved

leanprover-community-mathlib4-bot added the delegated label Jan 4, 2025

Update Mathlib/Algebra/DirectSum/Idempotents.lean

63dcdd9

Co-authored-by: Kevin Buzzard <[email protected]>

mathlib-bors bot pushed a commit that referenced this pull request Jan 4, 2025

feat(Algebra): more on OrthogonalIdempotents (#18195)

b43248b

Co-authored-by : @jjaassoonn Co-authored-by: Whysoserioushah <[email protected]>

mathlib-bors bot changed the title ~~feat(Algebra): more on OrthogonalIdempotents~~ [Merged by Bors] - feat(Algebra): more on OrthogonalIdempotents Jan 4, 2025

mathlib-bors bot closed this Jan 4, 2025

mathlib-bors bot deleted the Primitive-Idempotents branch January 4, 2025 19:04

alreadydone reviewed Jan 6, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Algebra): more on `OrthogonalIdempotents` #18195

[Merged by Bors] - feat(Algebra): more on `OrthogonalIdempotents` #18195

Whysoserioushah commented Oct 24, 2024 •

edited

Loading

github-actions bot commented Oct 24, 2024 •

edited

Loading

Declarations diff

erdOne left a comment

erdOne left a comment

kbuzzard commented Jan 4, 2025

mathlib-bors bot commented Jan 4, 2025

Whysoserioushah commented Jan 4, 2025

mathlib-bors bot commented Jan 4, 2025

alreadydone Jan 6, 2025

		theorem completeOrthogonalIdempotents_idempotent [Fintype I]:
		CompleteOrthogonalIdempotents fun i ↦ idempotent V i where

[Merged by Bors] - feat(Algebra): more on OrthogonalIdempotents #18195

[Merged by Bors] - feat(Algebra): more on OrthogonalIdempotents #18195

Conversation

Whysoserioushah commented Oct 24, 2024 • edited Loading

github-actions bot commented Oct 24, 2024 • edited Loading

PR summary 63dcdd9437

Import changes for modified files

Declarations diff

erdOne left a comment

Choose a reason for hiding this comment

erdOne left a comment

Choose a reason for hiding this comment

kbuzzard commented Jan 4, 2025

mathlib-bors bot commented Jan 4, 2025

Whysoserioushah commented Jan 4, 2025

mathlib-bors bot commented Jan 4, 2025

alreadydone Jan 6, 2025

Choose a reason for hiding this comment

[Merged by Bors] - feat(Algebra): more on `OrthogonalIdempotents` #18195

[Merged by Bors] - feat(Algebra): more on `OrthogonalIdempotents` #18195

Whysoserioushah commented Oct 24, 2024 •

edited

Loading

github-actions bot commented Oct 24, 2024 •

edited

Loading