Central idempotents

A central idempotent of a ring R is an element e with e * e = e that commutes with everything. Such an element splits R as a product of the two rings eR and (1 - e)R, so the central idempotents record how far R is from being indecomposable as a ring.

This file collects the three facts that make TauCeti.centralIdempotents a counting invariant. It is preserved by ring isomorphisms (RingEquiv.centralIdempotentsCongr); it is computed coordinatewise on a product (TauCeti.centralIdempotentsPiEquiv); and a simple ring has exactly two of them, 0 and 1 (TauCeti.centralIdempotents_eq_pair). Together these say that a finite product of simple rings has exactly 2 ^ (number of factors) central idempotents (TauCeti.card_centralIdempotents_pi_of_isSimpleRing), so the number of factors can be read off the isomorphism class of the ring alone. TauCeti/RingTheory/SimpleRing/Pi.lean obtains the stronger factor matching for arbitrary products directly from their coordinate central idempotents.

Mathlib has IsIdempotentElem and the orthogonal decompositions of 1 it generates (Mathlib/RingTheory/Idempotents.lean), and Subring.center, but nothing about the idempotents that are also central. The one nontrivial ingredient below, TauCeti.centralIdempotents_eq_pair, is the observation that a central idempotent of R is an idempotent of Subring.center R, which for simple R is a field by IsSimpleRing.isField_center; a field has only the idempotents 0 and 1.

The last section applies that dichotomy in the other direction: a surjection of algebras A × A ↠ B onto a simple B sends (1, 0) to a central idempotent, so one of the two blocks already maps onto B (AlgHom.exists_algHom_surjective_of_prod).

Main definitions

• TauCeti.centralIdempotents R: the set of central idempotents of R.
• RingEquiv.centralIdempotentsCongr: a ring isomorphism R ≃+* S restricts to an equivalence between the central idempotents of R and those of S.
• TauCeti.centralIdempotentsPiEquiv: the central idempotents of a product of rings are the families of central idempotents of the factors.

Main results

• TauCeti.centralIdempotents_eq_pair: a simple ring has exactly the two central idempotents 0 and 1, and TauCeti.card_centralIdempotents_of_isSimpleRing counts them.
• TauCeti.card_centralIdempotents_pi: the count is multiplicative over a finite product, whence TauCeti.card_centralIdempotents_pi_of_isSimpleRing: a finite product of simple rings has 2 ^ (number of factors) central idempotents.
• AlgHom.exists_algHom_surjective_of_prod: a surjection of algebras A × A ↠ B onto a simple ring restricts to a surjection along one of the two coordinates.

Implementation notes

centralIdempotents R is a Set R rather than a subtype or a bundled structure: the only thing done with it here is to transport it along isomorphisms and to count it, and Nat.card of the coercion is the count. Centrality is spelled as membership in Subring.center R, which is Mathlib's canonical form; TauCeti.mul_comm_of_mem_centralIdempotents unpacks it to the bare commutation equation.

def TauCeti.centralIdempotents (R : Type u_3) [Ring R] : Set R

The set of central idempotents of a ring: the idempotents lying in the centre.

Equations

• TauCeti.centralIdempotents R = {e : R | IsIdempotentElem e ∧ e ∈ Subring.center R}

theorem TauCeti.mem_centralIdempotents {R : Type u_1} [Ring R] {e : R} : e ∈ centralIdempotents R ↔ IsIdempotentElem e ∧ e ∈ Subring.center R

theorem TauCeti.isIdempotentElem_of_mem_centralIdempotents {R : Type u_1} [Ring R] {e : R} (he : e ∈ centralIdempotents R) : IsIdempotentElem e

A central idempotent is idempotent.

theorem TauCeti.mul_comm_of_mem_centralIdempotents {R : Type u_1} [Ring R] {e : R} (he : e ∈ centralIdempotents R) (x : R) : e * x = x * e

A central idempotent commutes with every element.

theorem TauCeti.zero_mem_centralIdempotents {R : Type u_1} [Ring R] : 0 ∈ centralIdempotents R

theorem TauCeti.one_mem_centralIdempotents {R : Type u_1} [Ring R] : 1 ∈ centralIdempotents R

theorem RingEquiv.map_mem_centralIdempotents {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R ≃+* S) {e : R} (he : e ∈ TauCeti.centralIdempotents R) : f e ∈ TauCeti.centralIdempotents S

A ring isomorphism preserves central idempotents.

def RingEquiv.centralIdempotentsCongr {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R ≃+* S) : ↑(TauCeti.centralIdempotents R) ≃ ↑(TauCeti.centralIdempotents S)

A ring isomorphism restricts to a bijection of central idempotents.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RingEquiv.coe_centralIdempotentsCongr_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R ≃+* S) (e : ↑(TauCeti.centralIdempotents R)) : ↑(f.centralIdempotentsCongr e) = f ↑e

@[simp]

theorem RingEquiv.coe_centralIdempotentsCongr_symm_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R ≃+* S) (e : ↑(TauCeti.centralIdempotents S)) : ↑(f.centralIdempotentsCongr.symm e) = f.symm ↑e

theorem RingEquiv.card_centralIdempotents_congr {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R ≃+* S) : Nat.card ↑(TauCeti.centralIdempotents R) = Nat.card ↑(TauCeti.centralIdempotents S)

Isomorphic rings have the same number of central idempotents.

@[simp]

theorem TauCeti.mem_centralIdempotents_pi {ι : Type u_2} (A : ι → Type u_3) [(i : ι) → Ring (A i)] {e : (i : ι) → A i} : e ∈ centralIdempotents ((i : ι) → A i) ↔ ∀ (i : ι), e i ∈ centralIdempotents (A i)

Both halves of being a central idempotent are coordinatewise conditions on a product of rings.

def TauCeti.centralIdempotentsPiEquiv {ι : Type u_2} (A : ι → Type u_3) [(i : ι) → Ring (A i)] : ↑(centralIdempotents ((i : ι) → A i)) ≃ ((i : ι) → ↑(centralIdempotents (A i)))

The central idempotents of a product of rings are the families of central idempotents.

Equations

• TauCeti.centralIdempotentsPiEquiv A = (Equiv.subtypeEquivRight ⋯).trans Equiv.subtypePiEquivPi

@[simp]

theorem TauCeti.coe_centralIdempotentsPiEquiv_apply {ι : Type u_2} (A : ι → Type u_3) [(i : ι) → Ring (A i)] (e : ↑(centralIdempotents ((i : ι) → A i))) (i : ι) : ↑((centralIdempotentsPiEquiv A) e i) = ↑e i

@[simp]

theorem TauCeti.coe_centralIdempotentsPiEquiv_symm_apply {ι : Type u_2} (A : ι → Type u_3) [(i : ι) → Ring (A i)] (e : (i : ι) → ↑(centralIdempotents (A i))) (i : ι) : ↑((centralIdempotentsPiEquiv A).symm e) i = ↑(e i)

theorem TauCeti.card_centralIdempotents_pi {ι : Type u_2} (A : ι → Type u_3) [(i : ι) → Ring (A i)] [Fintype ι] : Nat.card ↑(centralIdempotents ((i : ι) → A i)) = ∏ i : ι, Nat.card ↑(centralIdempotents (A i))

The number of central idempotents is multiplicative over a finite product of rings.

theorem TauCeti.centralIdempotents_eq_pair (R : Type u_1) [Ring R] [IsSimpleRing R] : centralIdempotents R = {0, 1}

A simple ring has exactly two central idempotents, 0 and 1.

A central idempotent of R is exactly an idempotent of the subring Subring.center R, which is a field because R is simple (IsSimpleRing.isField_center); and a field has no idempotents besides 0 and 1 (IsIdempotentElem.iff_eq_zero_or_one).

theorem TauCeti.card_centralIdempotents_of_isSimpleRing (R : Type u_1) [Ring R] [IsSimpleRing R] : Nat.card ↑(centralIdempotents R) = 2

A simple ring has exactly two central idempotents.

theorem TauCeti.card_centralIdempotents_pi_of_isSimpleRing {ι : Type u_2} [Finite ι] (A : ι → Type u_3) [(i : ι) → Ring (A i)] [∀ (i : ι), IsSimpleRing (A i)] : Nat.card ↑(centralIdempotents ((i : ι) → A i)) = 2 ^ Nat.card ι

A finite product of simple rings has 2 ^ (number of factors) central idempotents: one independent binary choice per factor.

A surjection onto a simple ring from a product of two copies of an algebra

theorem AlgHom.exists_algHom_surjective_of_prod {F : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring F] [Semiring A] [Algebra F A] [Ring B] [Algebra F B] [IsSimpleRing B] (φ : A × A →ₐ[F] B) (hφ : Function.Surjective ⇑φ) : ∃ (ψ : A →ₐ[F] B), Function.Surjective ⇑ψ

A surjection onto a simple ring from a product of two copies of an algebra factors through a coordinate. The image of (1, 0) is a central idempotent of B, hence 0 or 1 (TauCeti.centralIdempotents_eq_pair); whichever it is, one of the two coordinate maps a ↦ φ (a, 0), a ↦ φ (0, a) is an algebra map onto B.

This is what turns a two-block splitting of an algebra into a statement about a single block; it is used that way for an odd-dimensional Clifford algebra in TauCeti/RepresentationTheory/Spin/OddStructure.lean.