Documentation

Mathlib.Algebra.Algebra.Spectrum

Spectrum of an element in an algebra #

This file develops the basic theory of the spectrum of an element of an algebra. This theory will serve as the foundation for spectral theory in Banach algebras.

Main definitions #

Main statements #

Notations #

def resolventSet (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : A) :
Set R

Given a commutative ring R and an R-algebra A, the resolvent set of a : A is the Set R consisting of those r : R for which r•1 - a is a unit of the algebra A.

Equations
Instances For
    def spectrum (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : A) :
    Set R

    Given a commutative ring R and an R-algebra A, the spectrum of a : A is the Set R consisting of those r : R for which r•1 - a is not a unit of the algebra A.

    The spectrum is simply the complement of the resolvent set.

    Equations
    Instances For
      noncomputable def resolvent {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : A) (r : R) :
      A

      Given an a : A where A is an R-algebra, the resolvent is a map R → A which sends r : R to (algebraMap R A r - a)⁻¹ when r ∈ resolvent R A and 0 when r ∈ spectrum R A.

      Equations
      Instances For
        @[simp]
        theorem IsUnit.val_subInvSMul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r (algebraMap R A) s - a)) :
        h.subInvSMul = (algebraMap R A) s - r⁻¹ a
        @[simp]
        theorem IsUnit.val_inv_subInvSMul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r (algebraMap R A) s - a)) :
        h.subInvSMul⁻¹ = r h.unit⁻¹
        noncomputable def IsUnit.subInvSMul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r (algebraMap R A) s - a)) :

        The unit 1 - r⁻¹ • a constructed from r • 1 - a when the latter is a unit.

        Equations
        Instances For
          theorem spectrum.mem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} :
          r spectrum R a ¬IsUnit ((algebraMap R A) r - a)
          theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} :
          rspectrum R a IsUnit ((algebraMap R A) r - a)
          theorem spectrum.zero_mem_iff (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
          theorem spectrum.not_isUnit_of_zero_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
          0 spectrum R a¬IsUnit a

          Alias of the forward direction of spectrum.zero_mem_iff.

          theorem spectrum.zero_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
          ¬IsUnit a0 spectrum R a

          Alias of the reverse direction of spectrum.zero_mem_iff.

          theorem spectrum.zero_not_mem_iff (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
          0spectrum R a IsUnit a
          theorem spectrum.zero_not_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
          IsUnit a0spectrum R a

          Alias of the reverse direction of spectrum.zero_not_mem_iff.

          theorem spectrum.isUnit_of_zero_not_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
          0spectrum R aIsUnit a

          Alias of the forward direction of spectrum.zero_not_mem_iff.

          theorem spectrum.subset_singleton_zero_compl (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} (ha : IsUnit a) :
          theorem spectrum.mem_resolventSet_of_left_right_inverse {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} {b : A} {c : A} (h₁ : ((algebraMap R A) r - a) * b = 1) (h₂ : c * ((algebraMap R A) r - a) = 1) :
          theorem spectrum.mem_resolventSet_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} :
          @[simp]
          theorem spectrum.algebraMap_mem_iff (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} :
          theorem spectrum.of_algebraMap_mem (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} :
          (algebraMap R S) r spectrum S ar spectrum R a

          Alias of the forward direction of spectrum.algebraMap_mem_iff.

          theorem spectrum.algebraMap_mem (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} :
          r spectrum R a(algebraMap R S) r spectrum S a

          Alias of the reverse direction of spectrum.algebraMap_mem_iff.

          @[simp]
          theorem spectrum.preimage_algebraMap (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} :
          @[simp]
          theorem spectrum.resolventSet_of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [Subsingleton A] (a : A) :
          resolventSet R a = Set.univ
          @[simp]
          theorem spectrum.of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [Subsingleton A] (a : A) :
          theorem spectrum.resolvent_eq {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r : R} (h : r resolventSet R a) :
          theorem spectrum.units_smul_resolvent {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} :
          theorem spectrum.units_smul_resolvent_self {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {a : A} :
          r resolvent a r = resolvent (r⁻¹ a) 1
          theorem spectrum.isUnit_resolvent {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} :

          The resolvent is a unit when the argument is in the resolvent set.

          theorem spectrum.inv_mem_resolventSet {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {a : Aˣ} (h : r resolventSet R a) :
          theorem spectrum.inv_mem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {a : Aˣ} :
          r spectrum R a r⁻¹ spectrum R a⁻¹
          theorem spectrum.zero_mem_resolventSet_of_unit {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : Aˣ) :
          0 resolventSet R a
          theorem spectrum.ne_zero_of_mem_of_unit {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : Aˣ} {r : R} (hr : r spectrum R a) :
          r 0
          theorem spectrum.add_mem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r : R} {s : R} :
          r + s spectrum R a r spectrum R (-(algebraMap R A) s + a)
          theorem spectrum.add_mem_add_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r : R} {s : R} :
          r + s spectrum R ((algebraMap R A) s + a) r spectrum R a
          theorem spectrum.smul_mem_smul_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {s : R} {r : Rˣ} :
          r s spectrum R (r a) s spectrum R a
          theorem spectrum.unit_smul_eq_smul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : A) (r : Rˣ) :
          spectrum R (r a) = r spectrum R a
          theorem spectrum.unit_mem_mul_iff_mem_swap_mul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {b : A} {r : Rˣ} :
          r spectrum R (a * b) r spectrum R (b * a)
          theorem spectrum.preimage_units_mul_eq_swap_mul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {b : A} :
          Units.val ⁻¹' spectrum R (a * b) = Units.val ⁻¹' spectrum R (b * a)
          theorem spectrum.star_mem_resolventSet_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [InvolutiveStar R] [StarRing A] [StarModule R A] {r : R} {a : A} :
          theorem spectrum.map_star {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [InvolutiveStar R] [StarRing A] [StarModule R A] (a : A) :
          theorem spectrum.subset_subalgebra {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (a : S) :
          spectrum R a spectrum R a
          theorem spectrum.subset_starSubalgebra {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [StarRing R] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} (a : S) :
          spectrum R a spectrum R a
          theorem spectrum.singleton_add_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) :
          {r} + spectrum R a = spectrum R ((algebraMap R A) r + a)
          theorem spectrum.add_singleton_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) :
          spectrum R a + {r} = spectrum R (a + (algebraMap R A) r)
          theorem spectrum.vadd_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) :
          r +ᵥ spectrum R a = spectrum R ((algebraMap R A) r + a)
          theorem spectrum.neg_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) :
          theorem spectrum.singleton_sub_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) :
          {r} - spectrum R a = spectrum R ((algebraMap R A) r - a)
          theorem spectrum.sub_singleton_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) :
          spectrum R a - {r} = spectrum R (a - (algebraMap R A) r)
          @[simp]
          theorem spectrum.zero_eq {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] :
          spectrum 𝕜 0 = {0}

          Without the assumption Nontrivial A, then 0 : A would be invertible.

          @[simp]
          theorem spectrum.scalar_eq {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] (k : 𝕜) :
          spectrum 𝕜 ((algebraMap 𝕜 A) k) = {k}
          @[simp]
          theorem spectrum.one_eq {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] :
          spectrum 𝕜 1 = {1}
          theorem spectrum.smul_eq_smul {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] (k : 𝕜) (a : A) (ha : (spectrum 𝕜 a).Nonempty) :
          spectrum 𝕜 (k a) = k spectrum 𝕜 a

          the assumption (σ a).Nonempty is necessary and cannot be removed without further conditions on the algebra A and scalar field 𝕜.

          theorem spectrum.nonzero_mul_eq_swap_mul {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (b : A) :
          spectrum 𝕜 (a * b) \ {0} = spectrum 𝕜 (b * a) \ {0}
          theorem spectrum.map_inv {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : Aˣ) :
          (spectrum 𝕜 a)⁻¹ = spectrum 𝕜 a⁻¹
          theorem AlgHom.mem_resolventSet_apply {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (φ : F) {a : A} {r : R} (h : r resolventSet R a) :
          r resolventSet R (φ a)
          theorem AlgHom.spectrum_apply_subset {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (φ : F) (a : A) :
          spectrum R (φ a) spectrum R a
          theorem AlgHom.apply_mem_spectrum {F : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] [FunLike F A R] [AlgHomClass F R A R] [Nontrivial R] (φ : F) (a : A) :
          φ a spectrum R a
          @[simp]
          theorem AlgEquiv.spectrum_eq {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) (a : A) :
          spectrum R (f a) = spectrum R a