Idempotents in rings

The predicate IsIdempotentElem is defined for general monoids in Algebra/Ring/Idempotents.lean. In this file we provide various results regarding idempotent elements in rings.

Main definitions

• OrthogonalIdempotents: A family { eᵢ } of idempotent elements is orthogonal if eᵢ * eⱼ = 0 for all i ≠ j.
• CompleteOrthogonalIdempotents: A family { eᵢ } of orthogonal idempotent elements is complete if ∑ eᵢ = 1.

Main results

• CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker: If the kernel of f : R →+* S consists of nilpotent elements, and { eᵢ } is a family of complete orthogonal idempotents in the range of f, then { eᵢ } is the image of some complete orthogonal idempotents in R.
• existsUnique_isIdempotentElem_eq_of_ker_isNilpotent: If R is commutative and the kernel of f : R →+* S consists of nilpotent elements, then every idempotent in the range of f lifts to a unique idempotent in R.
• CompleteOrthogonalIdempotents.bijective_pi: If R is commutative, then a family { eᵢ } of complete orthogonal idempotent elements induces a ring isomorphism R ≃ ∏ R ⧸ ⟨1 - eᵢ⟩.

theorem isIdempotentElem_one_sub_one_sub_pow_pow {R : Type u_1} [Ring R] (x : R) (n : ℕ) (hx : (x - x ^ 2) ^ n = 0) : IsIdempotentElem (1 - (1 - x ^ n) ^ n)

theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (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

theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (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

Orthogonal idempotents lift along nil ideals.

theorem exists_isIdempotentElem_eq_of_ker_isNilpotent {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (e : S) (he : e ∈ f.range) (he' : IsIdempotentElem e) : ∃ (e' : R), IsIdempotentElem e' ∧ f e' = e

Idempotents lift along nil ideals.

theorem orthogonalIdempotents_iff {R : Type u_1} [Ring R] {I : Type u_3} (e : I → R) : OrthogonalIdempotents e ↔ (∀ (i : I), IsIdempotentElem (e i)) ∧ ∀ (i j : I), i ≠ j → e i * e j = 0

structure OrthogonalIdempotents {R : Type u_1} [Ring R] {I : Type u_3} (e : I → R) : Prop

A family { eᵢ } of idempotent elements is orthogonal if eᵢ * eⱼ = 0 for all i ≠ j.

• idem : ∀ (i : I), IsIdempotentElem (e i)
• ortho : ∀ (i j : I), i ≠ j → e i * e j = 0

theorem OrthogonalIdempotents.idem {R : Type u_1} [Ring R] {I : Type u_3} {e : I → R} (self : OrthogonalIdempotents e) (i : I) : IsIdempotentElem (e i)

theorem OrthogonalIdempotents.ortho {R : Type u_1} [Ring R] {I : Type u_3} {e : I → R} (self : OrthogonalIdempotents e) (i : I) (j : I) : i ≠ j → e i * e j = 0

theorem OrthogonalIdempotents.mul_eq {R : Type u_1} [Ring R] {I : Type u_3} {e : I → R} [DecidableEq I] (he : OrthogonalIdempotents e) (i : I) (j : I) : e i * e j = if i = j then e i else 0

theorem OrthogonalIdempotents.iff_mul_eq {R : Type u_1} [Ring R] {I : Type u_3} {e : I → R} [DecidableEq I] : OrthogonalIdempotents e ↔ ∀ (i j : I), e i * e j = if i = j then e i else 0

theorem OrthogonalIdempotents.isIdempotentElem_sum {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] {e : I → R} (he : OrthogonalIdempotents e) : IsIdempotentElem (∑ i : I, e i)

theorem OrthogonalIdempotents.map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {I : Type u_3} {e : I → R} (he : OrthogonalIdempotents e) : OrthogonalIdempotents (⇑f ∘ e)

theorem OrthogonalIdempotents.map_injective_iff {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {I : Type u_3} {e : I → R} (hf : Function.Injective ⇑f) : OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e

theorem OrthogonalIdempotents.embedding {R : Type u_1} [Ring R] {I : Type u_3} {e : I → R} (he : OrthogonalIdempotents e) {J : Type u_4} (i : J ↪ I) : OrthogonalIdempotents (e ∘ ⇑i)

theorem OrthogonalIdempotents.equiv {R : Type u_1} [Ring R] {I : Type u_3} {e : I → R} {J : Type u_4} (i : J ≃ I) : OrthogonalIdempotents (e ∘ ⇑i) ↔ OrthogonalIdempotents e

theorem OrthogonalIdempotents.unique {R : Type u_1} [Ring R] {I : Type u_3} {e : I → R} [Unique I] : OrthogonalIdempotents e ↔ IsIdempotentElem (e default)

theorem OrthogonalIdempotents.option {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] {e : I → R} (he : OrthogonalIdempotents e) (x : R) (hx : IsIdempotentElem x) (hx₁ : x * ∑ i : I, e i = 0) (hx₂ : (∑ i : I, e i) * x = 0) : OrthogonalIdempotents fun (x_1 : Option I) => x_1.elim x e

theorem OrthogonalIdempotents.lift_of_isNilpotent_ker_aux {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {n : ℕ} {e : Fin n → S} (he : OrthogonalIdempotents e) (he' : ∀ (i : Fin n), e i ∈ f.range) : ∃ (e' : Fin n → R), OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

theorem OrthogonalIdempotents.lift_of_isNilpotent_ker {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {I : Type u_3} [Fintype I] (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {e : I → S} (he : OrthogonalIdempotents e) (he' : ∀ (i : I), e i ∈ f.range) : ∃ (e' : I → R), OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

A family of orthogonal idempotents lift along nil ideals.

theorem completeOrthogonalIdempotents_iff {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] (e : I → R) : CompleteOrthogonalIdempotents e ↔ OrthogonalIdempotents e ∧ ∑ i : I, e i = 1

structure CompleteOrthogonalIdempotents {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] (e : I → R) extends OrthogonalIdempotents : Prop

A family { eᵢ } of idempotent elements is complete orthogonal if

1. (orthogonal) eᵢ * eⱼ = 0 for all i ≠ j.
2. (complete) ∑ eᵢ = 1

• idem : ∀ (i : I), IsIdempotentElem (e i)
• ortho : ∀ (i j : I), i ≠ j → e i * e j = 0
• complete : ∑ i : I, e i = 1

theorem CompleteOrthogonalIdempotents.complete {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] {e : I → R} (self : CompleteOrthogonalIdempotents e) : ∑ i : I, e i = 1

theorem CompleteOrthogonalIdempotents.unique_iff {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] {e : I → R} [Unique I] : CompleteOrthogonalIdempotents e ↔ e default = 1

theorem CompleteOrthogonalIdempotents.pair_iff {R : Type u_1} [Ring R] {x : R} {y : R} : CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x

theorem CompleteOrthogonalIdempotents.of_isIdempotentElem {R : Type u_1} [Ring R] {e : R} (he : IsIdempotentElem e) : CompleteOrthogonalIdempotents ![e, 1 - e]

theorem CompleteOrthogonalIdempotents.single {I : Type u_4} [Fintype I] [DecidableEq I] (R : I → Type u_5) [(i : I) → Ring (R i)] : CompleteOrthogonalIdempotents fun (x : I) => Pi.single x 1

theorem CompleteOrthogonalIdempotents.map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {I : Type u_3} [Fintype I] {e : I → R} (he : CompleteOrthogonalIdempotents e) : CompleteOrthogonalIdempotents (⇑f ∘ e)

theorem CompleteOrthogonalIdempotents.map_injective_iff {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {I : Type u_3} [Fintype I] {e : I → R} (hf : Function.Injective ⇑f) : CompleteOrthogonalIdempotents (⇑f ∘ e) ↔ CompleteOrthogonalIdempotents e

theorem CompleteOrthogonalIdempotents.equiv {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] {e : I → R} {J : Type u_4} [Fintype J] (i : J ≃ I) : CompleteOrthogonalIdempotents (e ∘ ⇑i) ↔ CompleteOrthogonalIdempotents e

theorem CompleteOrthogonalIdempotents.option {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] {e : I → R} (he : OrthogonalIdempotents e) : CompleteOrthogonalIdempotents fun (x : Option I) => x.elim (1 - ∑ i : I, e i) e

theorem CompleteOrthogonalIdempotents.of_subsingleton {R : Type u_1} [Ring R] {I : Type u_3} [Fintype I] {e : I → R} [Subsingleton R] : CompleteOrthogonalIdempotents e

theorem CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker_aux {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {n : ℕ} {e : Fin n → S} (he : CompleteOrthogonalIdempotents e) (he' : ∀ (i : Fin n), e i ∈ f.range) : ∃ (e' : Fin n → R), CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

theorem CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {I : Type u_3} [Fintype I] (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {e : I → S} (he : CompleteOrthogonalIdempotents e) (he' : ∀ (i : I), e i ∈ f.range) : ∃ (e' : I → R), CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

A system of complete orthogonal idempotents lift along nil ideals.

theorem eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute {R : Type u_1} [Ring R] {e₁ : R} {e₂ : R} (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂) (H : IsNilpotent (e₁ - e₂)) (H' : Commute e₁ e₂) : e₁ = e₂

theorem CompleteOrthogonalIdempotents.of_ker_isNilpotent_of_isMulCentral {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {I : Type u_3} [Fintype I] {e : I → R} (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (he : ∀ (i : I), IsIdempotentElem (e i)) (he' : ∀ (i : I), IsMulCentral (e i)) (he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)) : CompleteOrthogonalIdempotents e

theorem eq_of_isNilpotent_sub_of_isIdempotentElem {R : Type u_1} [CommRing R] {e₁ : R} {e₂ : R} (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂) (H : IsNilpotent (e₁ - e₂)) : e₁ = e₂

theorem existsUnique_isIdempotentElem_eq_of_ker_isNilpotent {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] (f : R →+* S) (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (e : S) (he : e ∈ f.range) (he' : IsIdempotentElem e) : ∃! e' : R, IsIdempotentElem e' ∧ f e' = e

theorem CompleteOrthogonalIdempotents.of_ker_isNilpotent {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] (f : R →+* S) {I : Type u_3} [Fintype I] {e : I → R} (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (he : ∀ (i : I), IsIdempotentElem (e i)) (he' : CompleteOrthogonalIdempotents (⇑f ∘ e)) : CompleteOrthogonalIdempotents e

theorem OrthogonalIdempotents.prod_one_sub {R : Type u_1} [CommRing R] {I : Type u_3} [Fintype I] {e : I → R} (he : OrthogonalIdempotents e) : ∏ i : I, (1 - e i) = 1 - ∑ i : I, e i

theorem CompleteOrthogonalIdempotents.prod_one_sub {R : Type u_1} [CommRing R] {I : Type u_3} [Fintype I] {e : I → R} (he : CompleteOrthogonalIdempotents e) : ∏ i : I, (1 - e i) = 0

theorem CompleteOrthogonalIdempotents.of_prod_one_sub {R : Type u_1} [CommRing R] {I : Type u_3} [Fintype I] {e : I → R} (he : OrthogonalIdempotents e) (he' : ∏ i : I, (1 - e i) = 0) : CompleteOrthogonalIdempotents e

theorem OrthogonalIdempotents.surjective_pi {R : Type u_1} [CommRing R] {I : Type u_3} [Fintype I] {e : I → R} (he : OrthogonalIdempotents e) : Function.Surjective ⇑(Pi.ringHom fun (i : I) => Ideal.Quotient.mk (Ideal.span {1 - e i}))

A family of orthogonal idempotents induces an surjection R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩

theorem CompleteOrthogonalIdempotents.bijective_pi {R : Type u_1} [CommRing R] {I : Type u_3} [Fintype I] {e : I → R} (he : CompleteOrthogonalIdempotents e) : Function.Bijective ⇑(Pi.ringHom fun (i : I) => Ideal.Quotient.mk (Ideal.span {1 - e i}))

A family of complete orthogonal idempotents induces an isomorphism R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩

theorem CompleteOrthogonalIdempotents.bijective_pi' {R : Type u_1} [CommRing R] {I : Type u_3} [Fintype I] {e : I → R} (he : CompleteOrthogonalIdempotents fun (x : I) => 1 - e x) : Function.Bijective ⇑(Pi.ringHom fun (i : I) => Ideal.Quotient.mk (Ideal.span {e i}))

theorem bijective_pi_of_isIdempotentElem {R : Type u_1} [CommRing R] {I : Type u_3} [Fintype I] (e : I → R) (he : ∀ (i : I), IsIdempotentElem (e i)) (he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0) (he₂ : ∏ i : I, e i = 0) : Function.Bijective ⇑(Pi.ringHom fun (i : I) => Ideal.Quotient.mk (Ideal.span {e i}))