Spectral idempotents of an element with a commuting partial inverse

Let C and b be commuting elements of a ring A with C ^ (h + 1) * b = C ^ h, that is, C ^ h * (C * b - 1) = 0. Then p = (C * b) ^ h is an idempotent, E = 1 - p is an idempotent killed by C ^ h, and w = b * p inverts C on the complementary summand:

C * w = w * C = 1 - E, E * w = w * E = 0.

So C is invertible in the corner p A p and nilpotent of order at most h in E A E. In the language of Drazin, w is the pseudo-inverse of C and E its spectral idempotent. For a compact operator u and a good zero a of its Fredholm determinant, C = 1 - a • u and b the normalised Hasse derivative of the Fredholm resolvent at a satisfy the hypothesis, and E is the Riesz projector onto the generalised eigenspace ker C ^ h.

The splitting is unique: two idempotents E₁, E₂, killed by C ^ h, such that C is invertible modulo each of them (C * wᵢ = wᵢ * C = 1 - Eᵢ), are equal (IsIdempotentElem.eq_of_pow_mul_eq_zero).

Main results

• TauCeti.pow_mul_mul_pow_of_pow_succ_mul_eq: C ^ h * (C * b) ^ n = C ^ h for every n.
• Commute.isIdempotentElem_mul_pow_of_pow_succ_mul_eq: (C * b) ^ h is idempotent.
• Commute.mul_mul_mul_pow_of_pow_succ_mul_eq, Commute.mul_mul_pow_mul_of_pow_succ_mul_eq: C * (b * (C * b) ^ h) = (C * b) ^ h and b * (C * b) ^ h * C = (C * b) ^ h.
• IsIdempotentElem.one_sub_eq_pow_mul_pow: if C ^ h * E = 0 and C * w = w * C = 1 - E for an idempotent E, then 1 - E = C ^ h * w ^ h.
• IsIdempotentElem.eq_of_pow_mul_eq_zero: uniqueness of the splitting.

References

• M. P. Drazin, Pseudo-inverses in associative rings and semigroups, Amer. Math. Monthly 65 (1958), 506–514.
• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §7.

theorem TauCeti.pow_mul_mul_pow_of_pow_succ_mul_eq {M : Type u_1} [Monoid M] {C b : M} {h : ℕ} (hb : C ^ (h + 1) * b = C ^ h) (n : ℕ) : C ^ h * (C * b) ^ n = C ^ h

If C ^ (h + 1) * b = C ^ h, then C ^ h * (C * b) ^ n = C ^ h for every n.

theorem Commute.mul_pow_add_of_pow_succ_mul_eq {M : Type u_1} [Monoid M] {C b : M} {h : ℕ} (hCb : Commute C b) (hb : C ^ (h + 1) * b = C ^ h) (n : ℕ) : (C * b) ^ (h + n) = (C * b) ^ h

If C and b commute and C ^ (h + 1) * b = C ^ h, then (C * b) ^ (h + n) = (C * b) ^ h for every n.

theorem Commute.isIdempotentElem_mul_pow_of_pow_succ_mul_eq {M : Type u_1} [Monoid M] {C b : M} {h : ℕ} (hCb : Commute C b) (hb : C ^ (h + 1) * b = C ^ h) : IsIdempotentElem ((C * b) ^ h)

If C and b commute and C ^ (h + 1) * b = C ^ h, then (C * b) ^ h is idempotent.

theorem Commute.mul_mul_mul_pow_of_pow_succ_mul_eq {M : Type u_1} [Monoid M] {C b : M} {h : ℕ} (hCb : Commute C b) (hb : C ^ (h + 1) * b = C ^ h) : C * (b * (C * b) ^ h) = (C * b) ^ h

If C and b commute and C ^ (h + 1) * b = C ^ h, then w = b * (C * b) ^ h satisfies C * w = (C * b) ^ h.

theorem Commute.mul_mul_pow_mul_of_pow_succ_mul_eq {M : Type u_1} [Monoid M] {C b : M} {h : ℕ} (hCb : Commute C b) (hb : C ^ (h + 1) * b = C ^ h) : b * (C * b) ^ h * C = (C * b) ^ h

If C and b commute and C ^ (h + 1) * b = C ^ h, then w = b * (C * b) ^ h satisfies w * C = (C * b) ^ h.

theorem IsIdempotentElem.isUnit_add_mul_one_sub {A : Type u_1} [Ring A] {C E w : A} (he : IsIdempotentElem E) (hw : C * w = 1 - E) (hw' : w * C = 1 - E) : IsUnit (E + C * (1 - E))

Replacing one block of a split operator by the identity gives a unit when the complementary block is invertible. The inverse is E + (1 - E) * w, where C * w = w * C = 1 - E.

theorem IsIdempotentElem.one_sub_eq_pow_mul_pow {A : Type u_1} [Ring A] {C E w : A} {h : ℕ} (he : IsIdempotentElem E) (hz : C ^ h * E = 0) (hw : C * w = 1 - E) (hw' : w * C = 1 - E) : 1 - E = C ^ h * w ^ h

Let E be an idempotent with C ^ h * E = 0, and let w invert C modulo E: C * w = w * C = 1 - E. Then 1 - E = C ^ h * w ^ h.

theorem IsIdempotentElem.eq_of_pow_mul_eq_zero {A : Type u_1} [Ring A] {C : A} {h : ℕ} {E₁ E₂ w₁ w₂ : A} (he₁ : IsIdempotentElem E₁) (he₂ : IsIdempotentElem E₂) (hz₁ : C ^ h * E₁ = 0) (hz₂ : C ^ h * E₂ = 0) (hw₁ : C * w₁ = 1 - E₁) (hw₁' : w₁ * C = 1 - E₁) (hw₂ : C * w₂ = 1 - E₂) (hw₂' : w₂ * C = 1 - E₂) : E₁ = E₂

Uniqueness of the spectral splitting. Let E₁ and E₂ be idempotents killed by C ^ h, such that C is invertible modulo each of them: C * wᵢ = wᵢ * C = 1 - Eᵢ. Then E₁ = E₂.