English
A complete orthogonal family of central idempotents e_i in a semiring R yields a direct product decomposition of R into the product of the corresponding corner rings. There exists a ring isomorphism R ≅ ∏_i (e_i R e_i).
Русский
Полное ортогональное семейство центральных идемпотентных элементов e_i в полусемиринге R дает прямое произведение угловых колец; существует изоморфизм колец R ≅ ∏_i (e_i R e_i).
LaTeX
$$$\\exists \\text{ ring isomorphism } R \\cong \\prod_{i} (e_i R e_i)\\,.$$$
Lean4
/-- A complete orthogonal family of central idempotents in a semiring
give rise to a direct product decomposition. -/
def ringEquivOfIsMulCentral [Semiring R] (he : CompleteOrthogonalIdempotents e) (hc : ∀ i, IsMulCentral (e i)) :
R ≃+* Π i, (he.idem i).Corner where
toFun r i := ⟨_, r, rfl⟩
invFun r := ∑ i, (r i).1
left_inv r := by simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]
right_inv
r :=
funext fun i ↦
Subtype.ext <| by
simp_rw [Finset.mul_sum, Finset.sum_mul]
rw [Finset.sum_eq_single i _ (by simp at ·)]
· have ⟨r', eq⟩ := (r i).2
rw [← eq]; simp_rw [← mul_assoc, (he.idem i).eq, mul_assoc, (he.idem i).eq]
· intro j _ ne; have ⟨r', eq⟩ := (r j).2
rw [← eq]; simp_rw [← mul_assoc, he.ortho ne.symm, zero_mul]
map_mul' r₁
r₂ :=
funext fun i ↦
Subtype.ext <|
calc
e i * (r₁ * r₂) * e i
_ = e i * (r₁ * e i * r₂) * e i := by simp_rw [← ((hc i).comm r₁).eq, ← mul_assoc, (he.idem i).eq]
_ = e i * r₁ * e i * (e i * r₂ * e i) :=
by
conv in (r₁ * _ * r₂) => rw [← (he.idem i).eq]
simp_rw [mul_assoc]
map_add' r₁ r₂ := funext fun i ↦ Subtype.ext <| by simpa [mul_add] using add_mul ..
