English
In a commutative semiring, a complete orthogonal family of idempotents yields a direct product decomposition of the ring into the product of its corner subrings.
Русский
В коммутативном полусемиринге полное ортогональное семейство идемпотентов дает разложение кольца на прямое произведение его угловых подкольцев.
LaTeX
$$$R \\text{ commutative semiring with } e_i \\text{ idempotent and complete orthogonal}, \\; R \\cong \\prod_i (e_i R e_i).$$$
Lean4
/-- A complete orthogonal family of idempotents in a commutative semiring
give rise to a direct product decomposition. -/
def ringEquivOfComm [CommSemiring R] (he : CompleteOrthogonalIdempotents e) : R ≃+* Π i, (he.idem i).Corner :=
he.ringEquivOfIsMulCentral fun _ ↦ Semigroup.mem_center_iff.mpr fun _ ↦ mul_comm ..
