From 48b78e8c21f26dc4cf9bcb02b32fdc4ecfc25f3f Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 6 Jan 2025 22:53:30 +0100 Subject: [PATCH] feat(RingTheory/Idempotents): generalize to Semiring, add Corner and direct product decomposition --- Mathlib/RingTheory/Idempotents.lean | 359 +++++++++++++++++++--------- 1 file changed, 243 insertions(+), 116 deletions(-) diff --git a/Mathlib/RingTheory/Idempotents.lean b/Mathlib/RingTheory/Idempotents.lean index c7b091ec93c93..9d42bb3accc80 100644 --- a/Mathlib/RingTheory/Idempotents.lean +++ b/Mathlib/RingTheory/Idempotents.lean @@ -35,74 +35,10 @@ In this file we provide various results regarding idempotent elements in rings. If `R` is commutative, then a family `{ eᵢ }` of complete orthogonal idempotent elements induces a ring isomorphism `R ≃ ∏ R ⧸ ⟨1 - eᵢ⟩`. -/ -section Ring -variable {R S : Type*} [Ring R] [Ring S] (f : R →+* S) - -theorem isIdempotentElem_one_sub_one_sub_pow_pow - (x : R) (n : ℕ) (hx : (x - x ^ 2) ^ n = 0) : - IsIdempotentElem (1 - (1 - x ^ n) ^ n) := by - let P : Polynomial ℤ := 1 - (1 - .X ^ n) ^ n - have : (.X - .X ^ 2) ^ n ∣ P - P ^ 2 := by - have H₁ : .X ^ n ∣ P := by - have := sub_dvd_pow_sub_pow 1 ((1 : Polynomial ℤ) - Polynomial.X ^ n) n - rwa [sub_sub_cancel, one_pow] at this - have H₂ : (1 - .X) ^ n ∣ 1 - P := by - simp only [sub_sub_cancel, P] - simpa using pow_dvd_pow_of_dvd (sub_dvd_pow_sub_pow (α := Polynomial ℤ) 1 Polynomial.X n) n - have := mul_dvd_mul H₁ H₂ - simpa only [← mul_pow, mul_sub, mul_one, ← pow_two] using this - have := map_dvd (Polynomial.aeval x) this - simp only [map_pow, map_sub, Polynomial.aeval_X, hx, map_one, zero_dvd_iff, P] at this - rwa [sub_eq_zero, eq_comm, pow_two] at this - -theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux - (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) - (e₁ : S) (he : e₁ ∈ f.range) (he₁ : IsIdempotentElem e₁) - (e₂ : R) (he₂ : IsIdempotentElem e₂) (he₁e₂ : e₁ * f e₂ = 0) : - ∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 := by - obtain ⟨e₁, rfl⟩ := he - cases subsingleton_or_nontrivial R - · exact ⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩ - let a := e₁ - e₁ * e₂ - have ha : f a = f e₁ := by rw [map_sub, map_mul, he₁e₂, sub_zero] - have ha' : a * e₂ = 0 := by rw [sub_mul, mul_assoc, he₂.eq, sub_self] - have hx' : a - a ^ 2 ∈ RingHom.ker f := by - simp [RingHom.mem_ker, mul_sub, pow_two, ha, he₁.eq] - obtain ⟨n, hn⟩ := h _ hx' - refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩ - · cases' n with n - · simp at hn - simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq, - he₁.one_sub.pow_succ_eq, sub_sub_cancel] - · obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n - apply_fun MulOpposite.unop at hk - have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk - rw [this, mul_assoc] - cases' n with n - · simp at hn - rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero] - -/-- Orthogonal idempotents lift along nil ideals. -/ -theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent - (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) - (e₁ : S) (he : e₁ ∈ f.range) (he₁ : IsIdempotentElem e₁) - (e₂ : R) (he₂ : IsIdempotentElem e₂) (he₁e₂ : e₁ * f e₂ = 0) (he₂e₁ : f e₂ * e₁ = 0) : - ∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0 := by - obtain ⟨e', h₁, rfl, h₂⟩ := exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux - f h e₁ he he₁ e₂ he₂ he₁e₂ - refine ⟨(1 - e₂) * e', ?_, ?_, ?_, ?_⟩ - · rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.eq] - · rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero] - · rw [mul_assoc, h₂, mul_zero] - · rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul] - -/-- Idempotents lift along nil ideals. -/ -theorem exists_isIdempotentElem_eq_of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) - (e : S) (he : e ∈ f.range) (he' : IsIdempotentElem e) : - ∃ e' : R, IsIdempotentElem e' ∧ f e' = e := by - simpa using exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h e he he' 0 .zero (by simp) +section Semiring +variable {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) variable {I : Type*} (e : I → R) /-- A family `{ eᵢ }` of idempotent elements is orthogonal if `eᵢ * eⱼ = 0` for all `i ≠ j`. -/ @@ -176,33 +112,6 @@ lemma OrthogonalIdempotents.option (he : OrthogonalIdempotents e) [Fintype I] (x Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, mul_zero] using congr_arg (e i * ·) hx₂ · exact he.ortho (Option.some_inj.ne.mp ne) -lemma OrthogonalIdempotents.lift_of_isNilpotent_ker_aux - (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) - {n} {e : Fin n → S} (he : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) : - ∃ e' : Fin n → R, OrthogonalIdempotents e' ∧ f ∘ e' = e := by - induction' n with n IH - · refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩ - · obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _) - have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i - obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ := - exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _ - h₁.isIdempotentElem_sum - (by simp [Finset.mul_sum, h₂', he.mul_eq, Fin.succ_ne_zero, eq_comm]) - (by simp [Finset.sum_mul, h₂', he.mul_eq, Fin.succ_ne_zero]) - refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩ - obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i <;> simp [*] - -/-- A family of orthogonal idempotents lift along nil ideals. -/ -lemma OrthogonalIdempotents.lift_of_isNilpotent_ker [Finite I] - (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) - {e : I → S} (he : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) : - ∃ e' : I → R, OrthogonalIdempotents e' ∧ f ∘ e' = e := by - cases nonempty_fintype I - obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h - (he.embedding (Fintype.equivFin I).symm.toEmbedding) (fun _ ↦ he' _) - refine ⟨_, h₁.embedding (Fintype.equivFin I).toEmbedding, - by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩ - variable [Fintype I] /-- @@ -214,31 +123,31 @@ A family `{ eᵢ }` of idempotent elements is complete orthogonal if structure CompleteOrthogonalIdempotents (e : I → R) extends OrthogonalIdempotents e : Prop where complete : ∑ i, e i = 1 +/-- If a family is complete orthogonal, it consists of idempotents. -/ +lemma CompleteOrthogonalIdempotents.iff_ortho_complete : + CompleteOrthogonalIdempotents e ↔ Pairwise (e · * e · = 0) ∧ ∑ i, e i = 1 := by + rw [completeOrthogonalIdempotents_iff, orthogonalIdempotents_iff, and_assoc, and_iff_right_of_imp] + intro ⟨ortho, complete⟩ i + apply_fun (e i * ·) at complete + rwa [Finset.mul_sum, Finset.sum_eq_single i (fun _ _ ne ↦ ortho ne.symm) (by simp at ·), mul_one] + at complete + +lemma CompleteOrthogonalIdempotents.pair_iff'ₛ {x y : R} : + CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1 := by + simp [iff_ortho_complete, Pairwise, Fin.forall_fin_two, and_assoc] + +lemma CompleteOrthogonalIdempotents.pair_iffₛ {R} [CommSemiring R] {x y : R} : + CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1 := by + rw [pair_iff'ₛ, and_left_comm, and_iff_right_of_imp]; exact (mul_comm x y ▸ ·.1) + lemma CompleteOrthogonalIdempotents.unique_iff [Unique I] : CompleteOrthogonalIdempotents e ↔ e default = 1 := by rw [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.unique, Fintype.sum_unique, and_iff_right_iff_imp] exact (· ▸ IsIdempotentElem.one) -lemma CompleteOrthogonalIdempotents.pair_iff {x y : R} : - CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x := by - rw [completeOrthogonalIdempotents_iff, orthogonalIdempotents_iff, and_assoc, Pairwise] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.forall_fin_two, Fin.isValue, - Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, ne_eq, not_true_eq_false, - false_implies, zero_ne_one, not_false_eq_true, true_implies, true_and, one_ne_zero, - and_true, and_self, Fin.sum_univ_two, eq_sub_iff_add_eq, @add_comm _ _ y] - constructor - · exact fun h ↦ ⟨h.1.1, h.2.2⟩ - · rintro ⟨h₁, h₂⟩ - obtain rfl := eq_sub_iff_add_eq'.mpr h₂ - exact ⟨⟨h₁, h₁.one_sub⟩, ⟨by simp [mul_sub, h₁.eq], by simp [sub_mul, h₁.eq]⟩, h₂⟩ - -lemma CompleteOrthogonalIdempotents.of_isIdempotentElem {e : R} (he : IsIdempotentElem e) : - CompleteOrthogonalIdempotents ![e, 1 - e] := - pair_iff.mpr ⟨he, rfl⟩ - lemma CompleteOrthogonalIdempotents.single {I : Type*} [Fintype I] [DecidableEq I] - (R : I → Type*) [∀ i, Ring (R i)] : + (R : I → Type*) [∀ i, Semiring (R i)] : CompleteOrthogonalIdempotents (Pi.single (f := R) · 1) := by refine ⟨⟨by simp [IsIdempotentElem, ← Pi.single_mul], ?_⟩, Finset.univ_sum_single 1⟩ intros i j hij @@ -262,6 +171,122 @@ lemma CompleteOrthogonalIdempotents.equiv {J} [Fintype J] (i : J ≃ I) : simp only [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.equiv, Function.comp_apply, and_congr_right_iff, Fintype.sum_equiv i _ e (fun _ ↦ rfl)] +@[nontriviality] +lemma CompleteOrthogonalIdempotents.of_subsingleton [Subsingleton R] : + CompleteOrthogonalIdempotents e := + ⟨⟨fun _ ↦ Subsingleton.elim _ _, fun _ _ _ ↦ Subsingleton.elim _ _⟩, Subsingleton.elim _ _⟩ + +end Semiring + +section Ring + +variable {R S : Type*} [Ring R] [Ring S] (f : R →+* S) + +theorem isIdempotentElem_one_sub_one_sub_pow_pow + (x : R) (n : ℕ) (hx : (x - x ^ 2) ^ n = 0) : + IsIdempotentElem (1 - (1 - x ^ n) ^ n) := by + let P : Polynomial ℤ := 1 - (1 - .X ^ n) ^ n + have : (.X - .X ^ 2) ^ n ∣ P - P ^ 2 := by + have H₁ : .X ^ n ∣ P := by + have := sub_dvd_pow_sub_pow 1 ((1 : Polynomial ℤ) - Polynomial.X ^ n) n + rwa [sub_sub_cancel, one_pow] at this + have H₂ : (1 - .X) ^ n ∣ 1 - P := by + simp only [sub_sub_cancel, P] + simpa using pow_dvd_pow_of_dvd (sub_dvd_pow_sub_pow (α := Polynomial ℤ) 1 Polynomial.X n) n + have := mul_dvd_mul H₁ H₂ + simpa only [← mul_pow, mul_sub, mul_one, ← pow_two] using this + have := map_dvd (Polynomial.aeval x) this + simp only [map_pow, map_sub, Polynomial.aeval_X, hx, map_one, zero_dvd_iff, P] at this + rwa [sub_eq_zero, eq_comm, pow_two] at this + +theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux + (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) + (e₁ : S) (he : e₁ ∈ f.range) (he₁ : IsIdempotentElem e₁) + (e₂ : R) (he₂ : IsIdempotentElem e₂) (he₁e₂ : e₁ * f e₂ = 0) : + ∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 := by + obtain ⟨e₁, rfl⟩ := he + cases subsingleton_or_nontrivial R + · exact ⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩ + let a := e₁ - e₁ * e₂ + have ha : f a = f e₁ := by rw [map_sub, map_mul, he₁e₂, sub_zero] + have ha' : a * e₂ = 0 := by rw [sub_mul, mul_assoc, he₂.eq, sub_self] + have hx' : a - a ^ 2 ∈ RingHom.ker f := by + simp [RingHom.mem_ker, mul_sub, pow_two, ha, he₁.eq] + obtain ⟨n, hn⟩ := h _ hx' + refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩ + · cases' n with n + · simp at hn + simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq, + he₁.one_sub.pow_succ_eq, sub_sub_cancel] + · obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n + apply_fun MulOpposite.unop at hk + have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk + rw [this, mul_assoc] + cases' n with n + · simp at hn + rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero] + +/-- Orthogonal idempotents lift along nil ideals. -/ +theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent + (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) + (e₁ : S) (he : e₁ ∈ f.range) (he₁ : IsIdempotentElem e₁) + (e₂ : R) (he₂ : IsIdempotentElem e₂) (he₁e₂ : e₁ * f e₂ = 0) (he₂e₁ : f e₂ * e₁ = 0) : + ∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0 := by + obtain ⟨e', h₁, rfl, h₂⟩ := exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux + f h e₁ he he₁ e₂ he₂ he₁e₂ + refine ⟨(1 - e₂) * e', ?_, ?_, ?_, ?_⟩ + · rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.eq] + · rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero] + · rw [mul_assoc, h₂, mul_zero] + · rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul] + +/-- Idempotents lift along nil ideals. -/ +theorem exists_isIdempotentElem_eq_of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) + (e : S) (he : e ∈ f.range) (he' : IsIdempotentElem e) : + ∃ e' : R, IsIdempotentElem e' ∧ f e' = e := by + simpa using exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h e he he' 0 .zero (by simp) + +lemma OrthogonalIdempotents.lift_of_isNilpotent_ker_aux + (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) + {n} {e : Fin n → S} (he : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) : + ∃ e' : Fin n → R, OrthogonalIdempotents e' ∧ f ∘ e' = e := by + induction' n with n IH + · refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩ + · obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _) + have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i + obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ := + exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _ + h₁.isIdempotentElem_sum + (by simp [Finset.mul_sum, h₂', he.mul_eq, Fin.succ_ne_zero, eq_comm]) + (by simp [Finset.sum_mul, h₂', he.mul_eq, Fin.succ_ne_zero]) + refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩ + obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i <;> simp [*] + +variable {I : Type*} {e : I → R} + +/-- A family of orthogonal idempotents lift along nil ideals. -/ +lemma OrthogonalIdempotents.lift_of_isNilpotent_ker [Finite I] + (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) + {e : I → S} (he : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) : + ∃ e' : I → R, OrthogonalIdempotents e' ∧ f ∘ e' = e := by + cases nonempty_fintype I + obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h + (he.embedding (Fintype.equivFin I).symm.toEmbedding) (fun _ ↦ he' _) + refine ⟨_, h₁.embedding (Fintype.equivFin I).toEmbedding, + by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩ + +lemma CompleteOrthogonalIdempotents.pair_iff {x y : R} : + CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x := by + rw [pair_iff'ₛ, ← eq_sub_iff_add_eq', ← and_assoc, and_congr_left_iff] + rintro rfl + simp [mul_sub, sub_mul, IsIdempotentElem, sub_eq_zero, eq_comm] + +lemma CompleteOrthogonalIdempotents.of_isIdempotentElem {e : R} (he : IsIdempotentElem e) : + CompleteOrthogonalIdempotents ![e, 1 - e] := + pair_iff.mpr ⟨he, rfl⟩ + +variable [Fintype I] + lemma CompleteOrthogonalIdempotents.option (he : OrthogonalIdempotents e) : CompleteOrthogonalIdempotents (Option.elim · (1 - ∑ i, e i) e) where __ := he.option _ he.isIdempotentElem_sum.one_sub @@ -270,11 +295,6 @@ lemma CompleteOrthogonalIdempotents.option (he : OrthogonalIdempotents e) : rw [Fintype.sum_option] exact sub_add_cancel _ _ -@[nontriviality] -lemma CompleteOrthogonalIdempotents.of_subsingleton [Subsingleton R] : - CompleteOrthogonalIdempotents e := - ⟨⟨fun _ ↦ Subsingleton.elim _ _, fun _ _ _ ↦ Subsingleton.elim _ _⟩, Subsingleton.elim _ _⟩ - lemma CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker_aux (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {n} {e : Fin n → S} (he : CompleteOrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) : @@ -426,3 +446,110 @@ lemma bijective_pi_of_isIdempotentElem (e : I → R) ⟨fun i ↦ (he i).one_sub, he₁⟩ (by simpa using he₂)).bijective_pi' end CommRing + +section corner + +variable {R : Type*} (e : R) + +namespace Subsemigroup + +variable [Semigroup R] + +/-- The corner associated to an element `e` in a semigroup +is the subsemigroup of all elements of the form `e * r * e`. -/ +def corner : Subsemigroup R where + carrier := Set.range (e * · * e) + mul_mem' := by rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a * e * e * b, by simp_rw [mul_assoc]⟩ + +variable {e} (idem : IsIdempotentElem e) +include idem + +lemma mem_corner_iff {r : R} : r ∈ corner e ↔ e * r = r ∧ r * e = r := + ⟨by rintro ⟨r, rfl⟩; simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and], + (⟨r, by simp_rw [·]⟩)⟩ + +lemma mem_corner_iff_mul_left (hc : IsMulCentral e) {r : R} : r ∈ corner e ↔ e * r = r := by + rw [mem_corner_iff idem, and_iff_left_of_imp]; intro; rwa [← hc.comm] + +lemma mem_corner_iff_mul_right (hc : IsMulCentral e) {r : R} : r ∈ corner e ↔ r * e = r := by + rw [mem_corner_iff_mul_left idem hc, hc.comm] + +lemma mem_corner_iff_mem_range_mul_left (hc : IsMulCentral e) {r : R} : + r ∈ corner e ↔ r ∈ Set.range (e * ·) := by + simp_rw [corner, mem_mk, Set.mem_range, ← hc.comm, ← mul_assoc, idem.eq] + +lemma mem_corner_iff_mem_range_mul_right (hc : IsMulCentral e) {r : R} : + r ∈ corner e ↔ r ∈ Set.range (· * e) := by + simp_rw [mem_corner_iff_mem_range_mul_left idem hc, hc.comm] + +/-- The corner associated to an idempotent `e` in a semiring without 1 +is the semiring with `e` as 1 consisting of all element of the form `e * r * e`. -/ +@[nolint unusedArguments] +def _root_.IsIdempotentElem.Corner (_ : IsIdempotentElem e) : Type _ := Subsemigroup.corner e + +end Subsemigroup + +/-- The corner associated to an element `e` in a semiring without 1 +is the subsemiring without 1 of all elements of the form `e * r * e`. -/ +def NonUnitalSubsemiring.corner [NonUnitalSemiring R] : NonUnitalSubsemiring R where + __ := Subsemigroup.corner e + add_mem' := by rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, by simp_rw [mul_add, add_mul]⟩ + zero_mem' := ⟨0, by simp_rw [mul_zero, zero_mul]⟩ + +/-- The corner associated to an element `e` in a ring without ` +is the subring without 1 of all elements of the form `e * r * e`. -/ +def NonUnitalRing.corner [NonUnitalRing R] : NonUnitalSubring R where + __ := NonUnitalSubsemiring.corner e + neg_mem' := by rintro _ ⟨a, rfl⟩; exact ⟨-a, by simp_rw [mul_neg, neg_mul]⟩ + +instance [NonUnitalSemiring R] (idem : IsIdempotentElem e) : Semiring idem.Corner where + __ : NonUnitalSemiring (NonUnitalSubsemiring.corner e) := inferInstance + one := ⟨e, e, by simp_rw [idem.eq]⟩ + one_mul r := Subtype.ext ((Subsemigroup.mem_corner_iff idem).mp r.2).1 + mul_one r := Subtype.ext ((Subsemigroup.mem_corner_iff idem).mp r.2).2 + +instance [NonUnitalCommSemiring R] (idem : IsIdempotentElem e) : CommSemiring idem.Corner where + __ : NonUnitalCommSemiring (NonUnitalSubsemiring.corner e) := inferInstance + __ : Semiring idem.Corner := inferInstance + +instance [NonUnitalRing R] (idem : IsIdempotentElem e) : Ring idem.Corner where + __ : NonUnitalRing (NonUnitalRing.corner e) := inferInstance + __ : Semiring idem.Corner := inferInstance + +instance [NonUnitalCommRing R] (idem : IsIdempotentElem e) : CommRing idem.Corner where + __ : NonUnitalCommRing (NonUnitalRing.corner e) := inferInstance + __ : Semiring idem.Corner := inferInstance + +variable {I : Type*} [Fintype I] {e : I → R} + +/-- A complete orthogonal family of central idempotents in a semiring +give rise to a direct product decomposition. -/ +def CompleteOrthogonalIdempotents.mulEquivOfIsMulCentral [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, 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₁, ← 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 .. + +/-- A complete orthogonal family of idempotents in a commutative semiring +give rise to a direct product decomposition. -/ +def CompleteOrthogonalIdempotents.mulEquivOfComm [CommSemiring R] + (he : CompleteOrthogonalIdempotents e) : R ≃+* Π i, (he.idem i).Corner := + he.mulEquivOfIsMulCentral fun _ ↦ Semigroup.mem_center_iff.mpr fun _ ↦ mul_comm .. + +end corner