[Merged by Bors] - feat(Order): Boolean algebra structure on idempotents by alreadydone · Pull Request #20618 · leanprover-community/mathlib4

alreadydone · 2025-01-09T20:51:45Z

We show that the idempotent in a commutative ring form a Boolean algebra, with complement given by a ↦ 1 - a and infimum given by multiplication. In a commutative semiring where subtraction is not available, it is still true that pairs of elements (a, b) satisfying a * b = 0 and a + b = 1 form a Boolean algebra (such elements are automatically idempotents, and such a pair is uniquely determined by either a or b).

github-actions · 2025-01-09T20:52:38Z

PR summary 015886aef7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Order.Idempotents` (new file)	233

Declarations diff

+ OrderIso.isIdempotentElemMulZeroAddOne
+ eq_of_mul_eq_add_eq_one
+ instance : BooleanAlgebra {a : α // IsIdempotentElem a}
+ instance : BooleanAlgebra {a : α × α // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1}
+ instance : Lattice {a : α // IsIdempotentElem a}
+ instance : PartialOrder {a : α × α // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1}
+ instance : SemilatticeSup {a : α × α // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1}
+ instance [CommMonoid α] : OrderTop {a : α // IsIdempotentElem a}
+ instance [CommMonoid α] [AddCommMonoid α] :
+ instance [CommMonoidWithZero α] : OrderBot {a : α // IsIdempotentElem a}
+ instance [CommSemigroup α] : SemilatticeInf {a : α // IsIdempotentElem a}
+ mul_eq_zero_add_eq_one_ext_left
+ mul_eq_zero_add_eq_one_ext_right
+ of_mul_add

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

mattrobball · 2025-01-10T20:16:46Z

Can you update the PR body with the main new declarations?

alreadydone · 2025-01-10T20:37:55Z

Can you update the PR body with the main new declarations?

I copied the module docstring, but didn't include the auto-generated instance names; I need to open an editor to find the names and I recall they're rather long. Should they be given names manually?

mattrobball · 2025-01-10T20:46:40Z

bors merge

We show that the idempotent in a commutative ring form a Boolean algebra, with complement given by `a ↦ 1 - a` and infimum given by multiplication. In a commutative semiring where subtraction is not available, it is still true that pairs of elements `(a, b)` satisfying `a * b = 0` and `a + b = 1` form a Boolean algebra (such elements are automatically idempotents, and such a pair is uniquely determined by either `a` or `b`).

mathlib-bors · 2025-01-10T21:19:01Z

Pull request successfully merged into master.

Build succeeded:

bryangingechen · 2025-01-10T21:19:42Z

This question is a bit late (and I haven't looked at the changes here in detail), but I wonder if it's worth connecting this with the material in Algebra.Ring.BooleanRing.

alreadydone · 2025-01-10T21:32:04Z

There is instBooleanRingAsBoolRing if you do want the Boolean ring structure with +, *. I do want the Boolean algebra structure with sup and inf here to build the OrderIsos with Clopens in PrimeSpectrum in #20533. (Interesting to note that the formula for sup is a+b-ab but for + it is a+b-2ab, because + is xor.

We show that the idempotent in a commutative ring form a Boolean algebra, with complement given by `a ↦ 1 - a` and infimum given by multiplication. In a commutative semiring where subtraction is not available, it is still true that pairs of elements `(a, b)` satisfying `a * b = 0` and `a + b = 1` form a Boolean algebra (such elements are automatically idempotents, and such a pair is uniquely determined by either `a` or `b`).

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

feat(Order): Boolean algebra structure on idempotents

5b9338a

alreadydone added t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Jan 9, 2025

alreadydone mentioned this pull request Jan 9, 2025

[Merged by Bors] - feat(PrimeSpectrum): Clopens in spectra of CommSemirings #20533

Closed

1 task

alreadydone mentioned this pull request Jan 9, 2025

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

Closed

alreadydone added 2 commits January 9, 2025 22:06

Mathlib.lean

40781c5

fix

015886a

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

mathlib-bors bot changed the title ~~feat(Order): Boolean algebra structure on idempotents~~ [Merged by Bors] - feat(Order): Boolean algebra structure on idempotents Jan 10, 2025

mathlib-bors bot closed this Jan 10, 2025

mathlib-bors bot deleted the BooleanAlgebra_idempotents branch January 10, 2025 21:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Order): Boolean algebra structure on idempotents#20618

[Merged by Bors] - feat(Order): Boolean algebra structure on idempotents#20618
alreadydone wants to merge 3 commits intomasterfrom
BooleanAlgebra_idempotents

alreadydone commented Jan 9, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 9, 2025 •

edited

Loading

Declarations diff

Uh oh!

mattrobball commented Jan 10, 2025

Uh oh!

alreadydone commented Jan 10, 2025

Uh oh!

mattrobball commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

bryangingechen commented Jan 10, 2025

Uh oh!

alreadydone commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 015886aef7

Import changes for modified files

Declarations diff

Uh oh!

mattrobball commented Jan 10, 2025

Uh oh!

alreadydone commented Jan 10, 2025

Uh oh!

mattrobball commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

bryangingechen commented Jan 10, 2025

Uh oh!

alreadydone commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

alreadydone commented Jan 9, 2025 •

edited

Loading

github-actions bot commented Jan 9, 2025 •

edited

Loading