Skip to content

[Merged by Bors] - feature(Algebra/Ring/Idempotents): product of an idempotent and its complement#20286

Closed
mans0954 wants to merge 8 commits intomasterfrom
mans0954/idempotent-mul_compl
Closed

[Merged by Bors] - feature(Algebra/Ring/Idempotents): product of an idempotent and its complement#20286
mans0954 wants to merge 8 commits intomasterfrom
mans0954/idempotent-mul_compl

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented Dec 28, 2024

Add a couple of simp lemmas. In a ring, the product of an idempotent and its complement is zero.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 28, 2024 •
edited
Loading

PR summary 222c211dbd

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ mul_one_sub_self
+ one_sub_mul_self

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Dec 28, 2024
loefflerd
loefflerd approved these changes Jan 9, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, just a couple of minor formatting nits.

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 9, 2025

🚀 Pull request has been placed on the maintainer queue by loefflerd.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 9, 2025
mans0954 and others added 2 commits January 9, 2025 19:38
@mans0954 @loefflerd
Update Mathlib/Algebra/Ring/Idempotents.lean
3daccb6 
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
@mans0954 @loefflerd
Update Mathlib/Algebra/Ring/Idempotents.lean
222c211 
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
@alreadydone
Copy link
Copy Markdown
Contributor

alreadydone commented Jan 9, 2025 •
edited
Loading

I've built a Boolean algebra out of idempotents in #20533 #20618. Potentially useful to you?
Looks like you've previously built IsLprojection.Subtype.BooleanAlgebra 😄 Should it be made a BooleanSubalgebra? (Update: oh I realized #20618 doesn't apply here because the ring isn't commutative (but the L-projections do commute with each other).)

jcommelin
jcommelin reviewed Jan 10, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 10, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 10, 2025
@mans0954
feature(Algebra/Ring/Idempotents): product of an idempotent and its c…
d14cbfb 
…omplement (#20286)

Add a couple of simp lemmas. In a ring, the product of an idempotent and its complement is zero.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 10, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feature(Algebra/Ring/Idempotents): product of an idempotent and its complement [Merged by Bors] - feature(Algebra/Ring/Idempotents): product of an idempotent and its complement Jan 10, 2025
@mathlib-bors mathlib-bors bot closed this Jan 10, 2025
@mathlib-bors mathlib-bors bot deleted the mans0954/idempotent-mul_compl branch January 10, 2025 08:14
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Jan 11, 2025 •
edited
Loading

I've built a Boolean algebra out of idempotents in #20533 #20618. Potentially useful to you? Looks like you've previously built IsLprojection.Subtype.BooleanAlgebra 😄 Should it be made a BooleanSubalgebra? (Update: oh I realized #20618 doesn't apply here because the ring isn't commutative (but the L-projections do commute with each other).)

I think it's still possible to engineer the situation you describe. Let X be a module over a ring M and let ℙᴸ[M](X) be the L-projections. Let N be the commutant of ℙᴸ[M](X) in M and let Z be the centre of N. Then ℙᴸ[M](X) is a Boolean subalgebra of the Boolean algebra of idempotents of Z.

This may not be entirely artificial - when X is a complex Banach Space, N would contain all of the Hermitian operators.

This raises some questions like "When do the Hermitian operators generate N? and "Are all projections in Z L-projections?" which I don't immediately know the answer to.

grunweg pushed a commit that referenced this pull request Jan 11, 2025
@mans0954 @grunweg
feature(Algebra/Ring/Idempotents): product of an idempotent and its c…
1e76a4e 
…omplement (#20286)

Add a couple of simp lemmas. In a ring, the product of an idempotent and its complement is zero.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Julian added a commit that referenced this pull request Jan 12, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
9ba6079 
* origin/master: (88 commits)
  chore(scripts): update nolints.json (#20672)
  chore: de-simp `map_eq_zero_iff_eq_one` (#20662)
  feat(Combinatorics/SimpleGraph): add independent sets (#18608)
  chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641)
  feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366)
  feat(AlgebraicTopology): model categories (#19158)
  chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548)
  feat(Data/List/ReduceOption): add replicate theorems (#20644)
  feat: approximate subgroups (#20050)
  feat: use scoped trace nodes in linarith (#19855)
  feat: disjoint union of charted spaces (#20619)
  feat: add some term elaborators for reduction (#15192)
  feat(Topology/Category): category of delta-generated spaces (#19499)
  add a variable_alias for Quantale and AddQuantale (#19282)
  feat(Computability/DFA): implement `isRegular_iff` (#19940)
  chore: unpin and bump batteries and importgraph (#20651)
  chore: split `Mathlib/Algebra/Group/Int` (#20624)
  feat: three lemmas related to Hausdorff distance (#20585)
  chore: `initialize_simps_projections` for `Submodule` (#20582)
  feat(Order): Boolean algebra structure on idempotents (#20618)
  chore(CategoryTheory): moving/renaming Subpresheaf (#20583)
  refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630)
  feat: sets of doubling strictly less than 3/2 (#20572)
  chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452)
  feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298)
  feat: product of subalgebras (#20202)
  feat: `Submodule.restrictScalars` commutes with `pow` (#20581)
  feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580)
  chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576)
  chore: use ofNat more (#20546)
  feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363)
  feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797)
  refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590)
  feat: Make `PNat.recOn` induction eliminator (#20617)
  feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608)
  feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574)
  feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573)
  chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611)
  feat: AbsoluteValue.IsNontrivial (#20588)
  chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092)
  chore(Data/Set): split the `CoeSort` instance to its own file (#19031)
  feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612)
  feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286)
  chore: cleanup more `erw` (#20601)
  chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587)
  chore: cleanup imports in PrimePow/Divisors (#20626)
  chore: split Algebra/BigOperators/Group/List (#20625)
  chore: reduce Topology->Order imports by moving content (#20627)
  chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592)
  refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@loefflerd loefflerd loefflerd approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mans0954 @alreadydone @loefflerd @jcommelin