The Gelfand radius of idempotents and of nonunital elements

The Gelfand radius gelfandRadius a of an element of a normed ring is the limit of ‖a ^ k‖ ^ (1 / k). A nonzero idempotent has Gelfand radius one, whatever its norm, since all of its positive powers coincide with it.

A nonunital algebra has no powers a ^ 0, so its Gelfand radius is computed in the ℓ¹ unitization WithLp 1 (Unitization ℂ A), into which A embeds isometrically. Gelfand's formula holds there: the spectral radius of a, the supremum of the moduli of its quasispectrum, is the Gelfand radius of its image in the unitization. Together these give a lower bound on spectral radii of elements of nonunital Banach algebras near a nonzero idempotent, which is how idempotents obstruct the separating spaces of algebra homomorphisms.

Main results

• IsIdempotentElem.gelfandRadius_eq_one: a nonzero idempotent has Gelfand radius one.
• IsIdempotentElem.one_le_gelfandRadius_mul_norm_inverse: a lower bound on the Gelfand radius of elements of the corner p R p.
• TauCeti.spectralRadius_eq_gelfandRadius_toLp_inr: Gelfand's formula for a nonunital complex Banach algebra, through its ℓ¹ unitization.

theorem IsIdempotentElem.gelfandRadius_eq_one {A : Type u_1} [NormedRing A] {p : A} (hp : IsIdempotentElem p) (h0 : p ≠ 0) : gelfandRadius p = 1

A nonzero idempotent has Gelfand radius one: all its positive powers are equal to it, so ‖p ^ k‖ ^ (1 / k) = ‖p‖ ^ (1 / k) tends to one. No normalization of the norm is needed.

theorem IsIdempotentElem.one_le_gelfandRadius_mul_norm_inverse {R : Type u_1} [NormedRing R] {p y : R} (hp : IsIdempotentElem p) (h0 : p ≠ 0) (hpy : p * y = y) (hyp : y * p = y) (hu : IsUnit (1 - p + y)) : 1 ≤ gelfandRadius y * ‖Ring.inverse (1 - p + y)‖

Elements of the corner p R p of a nonzero idempotent p are bounded away from quasinilpotence near p. If p * y = y = y * p and 1 - p + y is a unit, then y is p * (1 - p + y), and the Gelfand radius of y is at least ‖(1 - p + y)⁻¹‖⁻¹. As y tends to p, this lower bound tends to ‖1‖⁻¹.

theorem TauCeti.spectralRadius_eq_gelfandRadius_toLp_inr {A : Type u_1} [NonUnitalNormedRing A] [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] (a : A) : spectralRadius ℂ a = ENNReal.ofReal (gelfandRadius (WithLp.toLp 1 ↑a))

Gelfand's formula in a nonunital complex Banach algebra: the spectral radius of a, computed from its quasispectrum, is the Gelfand radius of its image in the ℓ¹ unitization.