Commit 2025-01-20 12:14 6313738a

View on Github →

feat(RingTheory/Idempotents): generalize to Semiring, add Corner and direct product decomposition (#20531)

  • Add CompleteOrthogonalIdempotents.iff_ortho_complete: if a family is complete orthogonal, it consists of idempotents.
  • Add CompleteOrthogonalIdempotents.pair_iff'ₛ: x and y form a complete orthogonal family iff x * y = y * x = 0 and x + y = 1. Golf pair_iff.
  • Given an element e in a semigroup R, define Subsemigroup.corner = eRe. If R is a non-unital semiring and e is an idempotent, then eRe is a semiring. Define IsIdempotentElem.Corner as the Type version of corner, and provide unital (commutative) (semi)ring instances on it.
  • CompleteOrthogonalIdempotents.mulEquivOfIsMulCentral: A complete orthogonal family of central idempotents in a semiring give rise to a direct product decomposition. There exists CompleteOrthogonalIdempotents.bijective_pi but it uses subtraction and quotient so it's not suitable for semirings.

Estimated changes