From ec8c697aeac7ea9d544d02ad76bb455f247d6ad3 Mon Sep 17 00:00:00 2001 From: Abhishek Shivakumar Date: Tue, 12 May 2026 20:46:35 +0100 Subject: [PATCH] feat(Algebra/Spectrum): add the second resolvent identity For `a b : A` in an `R`-algebra and `r` in the resolvent set of both, resolvent a r - resolvent b r = resolvent a r * (a - b) * resolvent b r. Companion to the first resolvent identity (resolvent_eq). --- Mathlib/Algebra/Algebra/Spectrum/Basic.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Algebra/Algebra/Spectrum/Basic.lean b/Mathlib/Algebra/Algebra/Spectrum/Basic.lean index c92c29f7a2d357..72f08084162abd 100644 --- a/Mathlib/Algebra/Algebra/Spectrum/Basic.lean +++ b/Mathlib/Algebra/Algebra/Spectrum/Basic.lean @@ -32,6 +32,7 @@ This theory will serve as the foundation for spectral theory in Banach algebras. * `spectrum.left_add_coset_eq`: elements of the scalar ring commute (addition) with the spectrum. * `spectrum.unit_mem_mul_comm` and `spectrum.preimage_units_mul_comm`: the units (of `R`) in `σ (a*b)` coincide with those in `σ (b*a)`. +* `spectrum.resolvent_sub_resolvent`: the second resolvent identity. * `spectrum.scalar_eq`: in a nontrivial algebra over a field, the spectrum of a scalar is a singleton. @@ -157,6 +158,21 @@ theorem of_subsingleton [Subsingleton A] (a : A) : spectrum R a = ∅ := by theorem resolvent_eq {a : A} {r : R} (h : r ∈ resolventSet R a) : resolvent a r = ↑h.unit⁻¹ := Ring.inverse_unit h.unit +/-- The second resolvent identity: for `r` in the resolvent set of both +`a` and `b`, +`resolvent a r - resolvent b r = resolvent a r * (a - b) * resolvent b r`. -/ +theorem resolvent_sub_resolvent {a b : A} {r : R} + (ha : r ∈ resolventSet R a) (hb : r ∈ resolventSet R b) : + resolvent a r - resolvent b r + = resolvent a r * (a - b) * resolvent b r := by + rw [resolvent_eq ha, resolvent_eq hb] + have h_units : (↑ha.unit⁻¹ : A) - (↑hb.unit⁻¹ : A) + = (↑ha.unit⁻¹ : A) * ((hb.unit : A) - (ha.unit : A)) * (↑hb.unit⁻¹ : A) := by + rw [mul_sub, sub_mul, mul_assoc, Units.mul_inv, mul_one, Units.inv_mul, one_mul] + have h_diff : (hb.unit : A) - (ha.unit : A) = a - b := by + rw [ha.unit_spec, hb.unit_spec]; abel + rw [h_units, h_diff] + theorem units_smul_resolvent {r : Rˣ} {s : R} {a : A} : r • resolvent a (s : R) = resolvent (r⁻¹ • a) (r⁻¹ • s : R) := by by_cases h : s ∈ spectrum R a