Mathlib.Algebra.Algebra.Spectrum.Basic

resolventSet definition

(a : A) : Set R

Full source

/-- 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`. -/
def resolventSet (a : A) : Set R :=
  {r : R | IsUnit (↑ₐ r - a)}

Resolvent set of an algebra element

Informal description

Given a commutative ring $R$ and an $R$-algebra $A$, the *resolvent set* of an element $a \in A$ is the set $\{r \in R \mid \text{algebraMap}(r) - a \text{ is a unit in } A\}$, where $\text{algebraMap} \colon R \to A$ is the canonical algebra homomorphism.

spectrum definition

(a : A) : Set R

Full source

/-- 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. -/
def spectrum (a : A) : Set R :=
  (resolventSet R a)ᶜ

Spectrum of an algebra element

Informal description

Given a commutative ring $R$ and an $R$-algebra $A$, the *spectrum* of an element $a \in A$ is the set $\sigma(a) = \{r \in R \mid \text{algebraMap}(r) - a \text{ is not a unit in } A\}$, where $\text{algebraMap} \colon R \to A$ is the canonical algebra homomorphism. The spectrum is the complement of the resolvent set of $a$.

resolvent definition

(a : A) (r : R) : A

Full source

/-- 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`. -/
noncomputable def resolvent (a : A) (r : R) : A :=
  Ring.inverse (↑ₐ r - a)

Resolvent function of an algebra element

Informal description

Given an element $a$ in an $R$-algebra $A$, the *resolvent* is a function $R \to A$ defined by \[ \text{resolvent}(a, r) = \begin{cases} (\text{algebraMap}(r) - a)^{-1} & \text{if } r \text{ is in the resolvent set of } a, \\ 0 & \text{if } r \text{ is in the spectrum of } a. \end{cases} \] Here, $\text{algebraMap} \colon R \to A$ is the canonical algebra homomorphism, and the resolvent set consists of all $r \in R$ for which $\text{algebraMap}(r) - a$ is invertible in $A$.

IsUnit.subInvSMul definition

{r : Rˣ} {s : R} {a : A} (h : IsUnit <| r • ↑ₐ s - a) : Aˣ

Full source

/-- The unit `1 - r⁻¹ • a` constructed from `r • 1 - a` when the latter is a unit. -/
@[simps]
noncomputable def IsUnit.subInvSMul {r : Rˣ} {s : R} {a : A} (h : IsUnit <| r • ↑ₐ s - a) : Aˣ where
  val := ↑ₐ s - r⁻¹ • a
  inv := r • ↑h.unit⁻¹
  val_inv := by rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
  inv_val := by rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]

Invertibility of algebra map difference with unit scalar

Informal description

Given a unit $r \in R^\times$, a scalar $s \in R$, and an element $a \in A$ in an $R$-algebra $A$, if the element $r \cdot \text{algebraMap}(s) - a$ is invertible, then the element $\text{algebraMap}(s) - r^{-1} \cdot a$ is also invertible, with its inverse given by $r \cdot (r \cdot \text{algebraMap}(s) - a)^{-1}$.

spectrum.mem_iff theorem

{r : R} {a : A} : r ∈ σ a ↔ ¬IsUnit (↑ₐ r - a)

Full source

theorem mem_iff {r : R} {a : A} : r ∈ σ ar ∈ σ a ↔ ¬IsUnit (↑ₐ r - a) :=
  Iff.rfl

Characterization of Spectrum Membership via Non-Units

Informal description

For an element $a$ in an $R$-algebra $A$ and a scalar $r \in R$, the scalar $r$ belongs to the spectrum $\sigma(a)$ of $a$ if and only if the element $\text{algebraMap}(r) - a$ is not a unit in $A$.

spectrum.not_mem_iff theorem

{r : R} {a : A} : r ∉ σ a ↔ IsUnit (↑ₐ r - a)

Full source

theorem not_mem_iff {r : R} {a : A} : r ∉ σ ar ∉ σ a ↔ IsUnit (↑ₐ r - a) := by
  apply not_iff_not.mp
  simp [Set.not_not_mem, mem_iff]

Characterization of Non-Spectrum Membership via Units

Informal description

For an element $a$ in an $R$-algebra $A$ and a scalar $r \in R$, the scalar $r$ does not belong to the spectrum $\sigma(a)$ of $a$ if and only if the element $\text{algebraMap}(r) - a$ is a unit in $A$.

spectrum.zero_mem_iff theorem

{a : A} : (0 : R) ∈ σ a ↔ ¬IsUnit a

Full source

theorem zero_mem_iff {a : A} : (0 : R) ∈ σ a(0 : R) ∈ σ a ↔ ¬IsUnit a := by
  rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]

Zero in Spectrum if and only if Non-Unit

Informal description

For an element $a$ in an $R$-algebra $A$, the scalar $0 \in R$ belongs to the spectrum $\sigma(a)$ of $a$ if and only if $a$ is not a unit in $A$.

spectrum.zero_not_mem_iff theorem

{a : A} : (0 : R) ∉ σ a ↔ IsUnit a

Full source

theorem zero_not_mem_iff {a : A} : (0 : R) ∉ σ a(0 : R) ∉ σ a ↔ IsUnit a := by
  rw [zero_mem_iff, Classical.not_not]

Zero Not in Spectrum if and only if Unit

Informal description

For an element $a$ in an $R$-algebra $A$, the scalar $0 \in R$ does not belong to the spectrum $\sigma(a)$ of $a$ if and only if $a$ is a unit in $A$.

Units.zero_not_mem_spectrum theorem

(a : Aˣ) : 0 ∉ spectrum R (a : A)

Full source

@[simp]
lemma _root_.Units.zero_not_mem_spectrum (a : Aˣ) : 0 ∉ spectrum R (a : A) :=
  spectrum.zero_not_mem R a.isUnit

Zero Excluded from Spectrum of Units

Informal description

For any unit $a$ in an $R$-algebra $A$, the scalar $0 \in R$ does not belong to the spectrum $\sigma(a)$ of $a$.

spectrum.subset_singleton_zero_compl theorem

{a : A} (ha : IsUnit a) : spectrum R a ⊆ {0}ᶜ

Full source

lemma subset_singleton_zero_compl {a : A} (ha : IsUnit a) : spectrumspectrum R a ⊆ {0}ᶜ :=
  Set.subset_compl_singleton_iff.mpr <| spectrum.zero_not_mem R ha

Spectrum of a Unit Excludes Zero

Informal description

For any unit element $a$ in an $R$-algebra $A$, the spectrum $\sigma(a)$ is contained in the complement of the singleton set $\{0\}$, i.e., $\sigma(a) \subseteq R \setminus \{0\}$.

spectrum.mem_resolventSet_of_left_right_inverse theorem

{r : R} {a b c : A} (h₁ : (↑ₐ r - a) * b = 1) (h₂ : c * (↑ₐ r - a) = 1) : r ∈ resolventSet R a

Full source

theorem mem_resolventSet_of_left_right_inverse {r : R} {a b c : A} (h₁ : (↑ₐ r - a) * b = 1)
    (h₂ : c * (↑ₐ r - a) = 1) : r ∈ resolventSet R a :=
  Units.isUnit ⟨↑ₐ r - a, b, h₁, by rwa [← left_inv_eq_right_inv h₂ h₁]⟩

Sufficient Condition for Membership in Resolvent Set via Left and Right Inverses

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any element $a \in A$ and scalar $r \in R$, if there exist elements $b, c \in A$ such that $( \text{algebraMap}(r) - a ) \cdot b = 1$ and $c \cdot ( \text{algebraMap}(r) - a ) = 1$, then $r$ belongs to the resolvent set of $a$.

spectrum.mem_resolventSet_iff theorem

{r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit (↑ₐ r - a)

Full source

theorem mem_resolventSet_iff {r : R} {a : A} : r ∈ resolventSet R ar ∈ resolventSet R a ↔ IsUnit (↑ₐ r - a) :=
  Iff.rfl

Characterization of Resolvent Set via Units: $r \in \rho(a) \iff \text{algebraMap}(r) - a$ is a unit

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any element $a \in A$ and scalar $r \in R$, the scalar $r$ belongs to the resolvent set of $a$ if and only if the element $\text{algebraMap}(r) - a$ is a unit in $A$, where $\text{algebraMap} \colon R \to A$ is the canonical algebra homomorphism.

spectrum.algebraMap_mem_iff theorem

 (S : Type*) {R A : Type*} [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 a ↔ r ∈ spectrum R a

Full source

@[simp]
theorem algebraMap_mem_iff (S : Type*) {R A : Type*} [CommSemiring R] [CommSemiring S]
    [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} :
    algebraMapalgebraMap R S r ∈ spectrum S aalgebraMap R S r ∈ spectrum S a ↔ r ∈ spectrum R a := by
  simp only [spectrum.mem_iff, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Spectrum Compatibility under Algebra Homomorphism in Scalar Tower

Informal description

Let $R$ and $S$ be commutative semirings, and let $A$ be a ring equipped with algebra structures over both $R$ and $S$, forming a scalar tower $R \to S \to A$. For any element $a \in A$ and any $r \in R$, the image of $r$ under the algebra homomorphism $\text{algebraMap} \colon R \to S$ belongs to the spectrum of $a$ in $S$ if and only if $r$ belongs to the spectrum of $a$ in $R$. In other words: \[ \text{algebraMap}(r) \in \sigma_S(a) \iff r \in \sigma_R(a). \]

spectrum.preimage_algebraMap theorem

 (S : Type*) {R A : Type*} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A]
  [IsScalarTower R S A] {a : A} : algebraMap R S ⁻¹' spectrum S a = spectrum R a

Full source

@[simp]
theorem preimage_algebraMap (S : Type*) {R A : Type*} [CommSemiring R] [CommSemiring S]
    [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} :
    algebraMapalgebraMap R S ⁻¹' spectrum S a = spectrum R a :=
  Set.ext fun _ => spectrum.algebraMap_mem_iff _

Preimage of Spectrum under Algebra Homomorphism Equals Base Spectrum in Scalar Tower

Informal description

Let $R$ and $S$ be commutative semirings, and let $A$ be a ring equipped with algebra structures over both $R$ and $S$, forming a scalar tower $R \to S \to A$. For any element $a \in A$, the preimage of the spectrum $\sigma_S(a)$ under the algebra homomorphism $\text{algebraMap} \colon R \to S$ equals the spectrum $\sigma_R(a)$. In other words: \[ \text{algebraMap}^{-1}(\sigma_S(a)) = \sigma_R(a). \]

spectrum.resolventSet_of_subsingleton theorem

[Subsingleton A] (a : A) : resolventSet R a = Set.univ

Full source

@[simp]
theorem resolventSet_of_subsingleton [Subsingleton A] (a : A) : resolventSet R a = Set.univ := by
  simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]

Resolvent Set of an Element in a Subsingleton Algebra is the Entire Scalar Ring

Informal description

For any algebra $A$ over a commutative semiring $R$, if $A$ is a subsingleton (i.e., has at most one element), then the resolvent set of any element $a \in A$ is the entire set $R$.

spectrum.of_subsingleton theorem

[Subsingleton A] (a : A) : spectrum R a = ∅

Full source

@[simp]
theorem of_subsingleton [Subsingleton A] (a : A) : spectrum R a = ∅ := by
  rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]

Spectrum of an Element in a Subsingleton Algebra is Empty

Informal description

For any algebra $A$ over a commutative semiring $R$, if $A$ is a subsingleton (i.e., has at most one element), then the spectrum of any element $a \in A$ is the empty set.

spectrum.resolvent_eq theorem

{a : A} {r : R} (h : r ∈ resolventSet R a) : resolvent a r = ↑h.unit⁻¹

Full source

theorem resolvent_eq {a : A} {r : R} (h : r ∈ resolventSet R a) : resolvent a r = ↑h.unit⁻¹ :=
  Ring.inverse_unit h.unit

Resolvent Function Equals Inverse of Unit for Elements in Resolvent Set

Informal description

For an element $a$ in an $R$-algebra $A$ and a scalar $r \in R$ in the resolvent set of $a$, the resolvent function satisfies $\text{resolvent}(a, r) = u^{-1}$, where $u$ is the unit corresponding to the invertible element $\text{algebraMap}(r) - a$ in $A$.

spectrum.units_smul_resolvent theorem

{r : Rˣ} {s : R} {a : A} : r • resolvent a (s : R) = resolvent (r⁻¹ • a) (r⁻¹ • s : R)

Full source

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
  · rw [mem_iff] at h
    simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
    rw [smul_assoc, ← smul_sub]
    have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu =>
      h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
    simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]
  · simp only [resolvent]
    have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
      simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h
    rw [← h'.val_subInvSMul, ← (not_mem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit,
      h'.val_inv_subInvSMul]
    simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]

Scalar Multiplication of Resolvent by Unit: $r \cdot \text{resolvent}(a, s) = \text{resolvent}(r^{-1} \cdot a, r^{-1} \cdot s)$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any unit $r \in R^\times$, scalar $s \in R$, and element $a \in A$, the following equality holds: \[ r \cdot \text{resolvent}(a, s) = \text{resolvent}(r^{-1} \cdot a, r^{-1} \cdot s). \] Here, $\text{resolvent}(a, s)$ denotes the resolvent function of $a$ at $s$, which is defined as $(\text{algebraMap}(s) - a)^{-1}$ when $s$ is in the resolvent set of $a$.

spectrum.units_smul_resolvent_self theorem

{r : Rˣ} {a : A} : r • resolvent a (r : R) = resolvent (r⁻¹ • a) (1 : R)

Full source

theorem units_smul_resolvent_self {r : Rˣ} {a : A} :
    r • resolvent a (r : R) = resolvent (r⁻¹ • a) (1 : R) := by
  simpa only [Units.smul_def, Algebra.id.smul_eq_mul, Units.inv_mul] using
    @units_smul_resolvent _ _ _ _ _ r r a

Resolvent Identity for Unit Scalar Multiplication: $r \cdot \text{resolvent}(a, r) = \text{resolvent}(r^{-1} \cdot a, 1)$

Informal description

For any unit $r$ in the commutative semiring $R$ and any element $a$ in the $R$-algebra $A$, the scalar multiplication of the resolvent of $a$ at $r$ by $r$ equals the resolvent of $r^{-1} \cdot a$ at $1$, i.e., \[ r \cdot \text{resolvent}(a, r) = \text{resolvent}(r^{-1} \cdot a, 1). \] Here, $\text{resolvent}(a, r)$ denotes the inverse of $\text{algebraMap}(r) - a$ when $r$ is in the resolvent set of $a$.

spectrum.isUnit_resolvent theorem

{r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit (resolvent a r)

Full source

/-- The resolvent is a unit when the argument is in the resolvent set. -/
theorem isUnit_resolvent {r : R} {a : A} : r ∈ resolventSet R ar ∈ resolventSet R a ↔ IsUnit (resolvent a r) :=
  isUnit_ringInverse.symm

Characterization of Resolvent Set via Unit Condition: $r \in \text{resolventSet}(a) \leftrightarrow \text{resolvent}(a, r) \text{ is a unit}$

Informal description

For any element $a$ in an $R$-algebra $A$ and any scalar $r \in R$, the scalar $r$ belongs to the resolvent set of $a$ if and only if the resolvent $\text{resolvent}(a, r)$ is a unit in $A$. Here, the resolvent set $\text{resolventSet}(a)$ consists of all $r \in R$ such that $\text{algebraMap}(r) - a$ is invertible in $A$, and $\text{resolvent}(a, r)$ is defined as the inverse of $\text{algebraMap}(r) - a$ when $r$ is in the resolvent set.

spectrum.inv_mem_resolventSet theorem

{r : Rˣ} {a : Aˣ} (h : (r : R) ∈ resolventSet R (a : A)) : (↑r⁻¹ : R) ∈ resolventSet R (↑a⁻¹ : A)

Full source

theorem inv_mem_resolventSet {r : Rˣ} {a : Aˣ} (h : (r : R) ∈ resolventSet R (a : A)) :
    (↑r⁻¹ : R) ∈ resolventSet R (↑a⁻¹ : A) := by
  rw [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, ← Units.smul_def] at h ⊢
  rw [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv, IsUnit.sub_iff]
  have h₁ : (a : A) * (r • (↑a⁻¹ : A) - 1) = r • (1 : A) - a := by
    rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
  have h₂ : (r • (↑a⁻¹ : A) - 1) * a = r • (1 : A) - a := by
    rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
  have hcomm : Commute (a : A) (r • (↑a⁻¹ : A) - 1) := by rwa [← h₂] at h₁
  exact (hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2

Inversion of Units in Resolvent Sets: $r \in \rho(a) \Rightarrow r^{-1} \in \rho(a^{-1})$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any unit $r \in R^\times$ and any unit $a \in A^\times$, if $r$ belongs to the resolvent set of $a$ (i.e., $\text{algebraMap}(r) - a$ is a unit in $A$), then the inverse $r^{-1}$ belongs to the resolvent set of $a^{-1}$ (i.e., $\text{algebraMap}(r^{-1}) - a^{-1}$ is a unit in $A$).

spectrum.inv_mem_iff theorem

{r : Rˣ} {a : Aˣ} : (r : R) ∈ σ (a : A) ↔ (↑r⁻¹ : R) ∈ σ (↑a⁻¹ : A)

Full source

theorem inv_mem_iff {r : Rˣ} {a : Aˣ} : (r : R) ∈ σ (a : A)(r : R) ∈ σ (a : A) ↔ (↑r⁻¹ : R) ∈ σ (↑a⁻¹ : A) :=
  not_iff_not.2 <| ⟨inv_mem_resolventSet, inv_mem_resolventSet⟩

Spectrum Inversion Property for Units: $r \in \sigma(a) \leftrightarrow r^{-1} \in \sigma(a^{-1})$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any unit $r \in R^\times$ and any unit $a \in A^\times$, the scalar $r$ belongs to the spectrum $\sigma(a)$ if and only if the inverse $r^{-1}$ belongs to the spectrum $\sigma(a^{-1})$.

spectrum.zero_mem_resolventSet_of_unit theorem

(a : Aˣ) : 0 ∈ resolventSet R (a : A)

Full source

theorem zero_mem_resolventSet_of_unit (a : Aˣ) : 0 ∈ resolventSet R (a : A) := by
  simpa only [mem_resolventSet_iff, ← not_mem_iff, zero_not_mem_iff] using a.isUnit

Zero is in the resolvent set of a unit element

Informal description

For any unit $a$ in an $R$-algebra $A$, the scalar $0$ belongs to the resolvent set of $a$, i.e., $0 \in \text{resolventSet}_R(a)$. This means that $\text{algebraMap}(0) - a$ is a unit in $A$.

spectrum.ne_zero_of_mem_of_unit theorem

{a : Aˣ} {r : R} (hr : r ∈ σ (a : A)) : r ≠ 0

Full source

theorem ne_zero_of_mem_of_unit {a : Aˣ} {r : R} (hr : r ∈ σ (a : A)) : r ≠ 0 := fun hn =>
  (hn ▸ hr) (zero_mem_resolventSet_of_unit a)

Nonzero Spectrum for Unit Elements: $r \in \sigma(a) \Rightarrow r \neq 0$ when $a$ is a unit

Informal description

For any unit $a$ in an $R$-algebra $A$ and any scalar $r \in R$, if $r$ belongs to the spectrum $\sigma(a)$, then $r$ is nonzero.

spectrum.add_mem_iff theorem

{a : A} {r s : R} : r + s ∈ σ a ↔ r ∈ σ (-↑ₐ s + a)

Full source

theorem add_mem_iff {a : A} {r s : R} : r + s ∈ σ ar + s ∈ σ a ↔ r ∈ σ (-↑ₐ s + a) := by
  simp only [mem_iff, sub_neg_eq_add, ← sub_sub, map_add]

Spectrum Shift Identity: $r + s \in \sigma(a) \leftrightarrow r \in \sigma(-\text{algebraMap}(s) + a)$

Informal description

Let $A$ be an algebra over a commutative ring $R$, and let $a \in A$. For any $r, s \in R$, the element $r + s$ belongs to the spectrum $\sigma(a)$ if and only if $r$ belongs to the spectrum $\sigma(-\text{algebraMap}(s) + a)$.

spectrum.add_mem_add_iff theorem

{a : A} {r s : R} : r + s ∈ σ (↑ₐ s + a) ↔ r ∈ σ a

Full source

theorem add_mem_add_iff {a : A} {r s : R} : r + s ∈ σ (↑ₐ s + a)r + s ∈ σ (↑ₐ s + a) ↔ r ∈ σ a := by
  rw [add_mem_iff, neg_add_cancel_left]

Spectrum Shift Identity: $r + s \in \sigma(s + a) \leftrightarrow r \in \sigma(a)$

Informal description

Let $A$ be an algebra over a commutative ring $R$, and let $a \in A$. For any $r, s \in R$, the element $r + s$ belongs to the spectrum $\sigma(\text{algebraMap}(s) + a)$ if and only if $r$ belongs to the spectrum $\sigma(a)$.

spectrum.smul_mem_smul_iff theorem

{a : A} {s : R} {r : Rˣ} : r • s ∈ σ (r • a) ↔ s ∈ σ a

Full source

theorem smul_mem_smul_iff {a : A} {s : R} {r : Rˣ} : r • s ∈ σ (r • a)r • s ∈ σ (r • a) ↔ s ∈ σ a := by
  simp only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub,
    isUnit_smul_iff]

Spectrum Scalar Equivalence: $r \cdot s \in \sigma(r \cdot a) \leftrightarrow s \in \sigma(a)$ for Units $r$

Informal description

Let $A$ be an algebra over a commutative semiring $R$, and let $a \in A$. For any scalar $s \in R$ and any unit $r \in R^\times$, the element $r \cdot s$ belongs to the spectrum $\sigma(r \cdot a)$ if and only if $s$ belongs to the spectrum $\sigma(a)$. In other words, $r \cdot s \in \sigma(r \cdot a) \leftrightarrow s \in \sigma(a)$.

spectrum.unit_smul_eq_smul theorem

(a : A) (r : Rˣ) : σ (r • a) = r • σ a

Full source

theorem unit_smul_eq_smul (a : A) (r : Rˣ) : σ (r • a) = r • σ a := by
  ext x
  have x_eq : x = r • r⁻¹ • x := by simp
  nth_rw 1 [x_eq]
  rw [smul_mem_smul_iff]
  constructor
  · exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
  · rintro ⟨w, _, (x'_eq : r • w = x)⟩
    simpa [← x'_eq ]

Spectrum Scaling by Units: $\sigma(r \cdot a) = r \cdot \sigma(a)$

Informal description

Let $A$ be an algebra over a commutative semiring $R$, and let $a \in A$. For any unit $r \in R^\times$, the spectrum of $r \cdot a$ is equal to $r$ multiplied by the spectrum of $a$, i.e., \[ \sigma(r \cdot a) = r \cdot \sigma(a). \]

spectrum.unit_mem_mul_comm theorem

{a b : A} {r : Rˣ} : ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)

Full source

theorem unit_mem_mul_comm {a b : A} {r : Rˣ} : ↑r ∈ σ (a * b)↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a) := by
  have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) := by
    refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
    · calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
    · calc
        (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
  have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
  rw [mul_smul_comm r⁻¹ b a] at this
  simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def,
    IsUnit.smul_sub_iff_sub_inv_smul, smul_mul_assoc]

Spectrum of Commuted Products: $r \in \sigma(a * b) \leftrightarrow r \in \sigma(b * a)$ for Units $r$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any elements $a, b \in A$ and any unit $r \in R^\times$, the unit $r$ belongs to the spectrum of $a * b$ if and only if it belongs to the spectrum of $b * a$. In other words, $r \in \sigma(a * b) \leftrightarrow r \in \sigma(b * a)$.

spectrum.preimage_units_mul_comm theorem

(a b : A) : ((↑) : Rˣ → R) ⁻¹' σ (a * b) = (↑) ⁻¹' σ (b * a)

Full source

theorem preimage_units_mul_comm (a b : A) :
    ((↑) : Rˣ → R) ⁻¹' σ (a * b) = (↑) ⁻¹' σ (b * a) :=
  Set.ext fun _ => unit_mem_mul_comm

Preimage of Spectrum under Units for Commuted Products: $\sigma(a * b) \cap R^\times = \sigma(b * a) \cap R^\times$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any elements $a, b \in A$, the preimage under the canonical inclusion $R^\times \to R$ of the spectrum of $a * b$ is equal to the preimage of the spectrum of $b * a$. In other words, \[ \sigma(a * b) \cap R^\times = \sigma(b * a) \cap R^\times. \]

spectrum.setOf_isUnit_inter_mul_comm theorem

(a b : A) : {r | IsUnit r} ∩ σ (a * b) = {r | IsUnit r} ∩ σ (b * a)

Full source

theorem setOf_isUnit_inter_mul_comm (a b : A) :
    {r | IsUnit r}{r | IsUnit r} ∩ σ (a * b) = {r | IsUnit r}{r | IsUnit r} ∩ σ (b * a) := by
  ext r
  simpa using fun hr : IsUnit r ↦ unit_mem_mul_comm (r := hr.unit)

Intersection of Units with Spectrum is Commutative under Product: $\{r \mid r \text{ unit}\} \cap \sigma(a * b) = \{r \mid r \text{ unit}\} \cap \sigma(b * a)$

Informal description

For any elements $a$ and $b$ in an $R$-algebra $A$, the intersection of the set of units in $R$ with the spectrum of $a * b$ is equal to the intersection of the set of units in $R$ with the spectrum of $b * a$. In other words, \[ \{r \in R \mid r \text{ is a unit}\} \cap \sigma(a * b) = \{r \in R \mid r \text{ is a unit}\} \cap \sigma(b * a). \]

spectrum.star_mem_resolventSet_iff theorem

{r : R} {a : A} : star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

Full source

theorem star_mem_resolventSet_iff {r : R} {a : A} :
    starstar r ∈ resolventSet R astar r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a) := by
  refine ⟨fun h => ?_, fun h => ?_⟩ <;>
    simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul,
      star_star, star_one] using IsUnit.star h

Star Operation and Resolvent Set: $\star r \in \rho(a) \leftrightarrow r \in \rho(\star a)$

Informal description

Let $R$ be a commutative ring with a star operation (involution), and let $A$ be an $R$-algebra. For any element $a \in A$ and any $r \in R$, the element $\star r$ is in the resolvent set of $a$ if and only if $r$ is in the resolvent set of $\star a$. In other words, \[ \star r \in \rho(a) \leftrightarrow r \in \rho(\star a), \] where $\rho(a)$ denotes the resolvent set of $a$.

spectrum.map_star theorem

(a : A) : σ (star a) = star (σ a)

Full source

protected theorem map_star (a : A) : σ (star a) = star (σ a) := by
  ext
  simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolventSet_iff.symm

Spectrum Invariance Under Star Operation: $\sigma(\star a) = \star(\sigma(a))$

Informal description

Let $R$ be a commutative ring with a star operation (involution), and let $A$ be an $R$-algebra. For any element $a \in A$, the spectrum of $\star a$ is equal to the image of the spectrum of $a$ under the star operation. In other words, \[ \sigma(\star a) = \star(\sigma(a)), \] where $\sigma(a)$ denotes the spectrum of $a$.

spectrum.subset_subalgebra theorem

 {S R A : Type*} [CommSemiring R] [Ring A] [Algebra R A] [SetLike S A] [SubringClass S A] [SMulMemClass S R A] {s : S}
  (a : s) : spectrum R (a : A) ⊆ spectrum R a

Full source

theorem subset_subalgebra {S R A : Type*} [CommSemiring R] [Ring A] [Algebra R A]
    [SetLike S A] [SubringClass S A] [SMulMemClass S R A] {s : S} (a : s) :
    spectrumspectrum R (a : A) ⊆ spectrum R a :=
  Set.compl_subset_compl.mpr fun _ ↦ IsUnit.map (SubalgebraClass.val s)

Spectrum Inclusion for Subalgebra Elements

Informal description

Let $R$ be a commutative semiring, $A$ a ring with an $R$-algebra structure, and $S$ a type of subsets of $A$ that forms a subring and is closed under scalar multiplication. For any element $a$ in a subset $s \in S$, the spectrum of $a$ viewed as an element of $A$ is contained in the spectrum of $a$ viewed as an element of $s$. In symbols: $$ \sigma_A(a) \subseteq \sigma_s(a). $$

spectrum.singleton_add_eq theorem

(a : A) (r : R) : { r } + σ a = σ (↑ₐ r + a)

Full source

theorem singleton_add_eq (a : A) (r : R) : {r} + σ a = σ (↑ₐ r + a) :=
  ext fun x => by
    rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]

Spectrum Shift Identity: $\{r\} + \sigma(a) = \sigma(\text{algebraMap}(r) + a)$

Informal description

Let $A$ be an algebra over a commutative ring $R$, and let $a \in A$. For any $r \in R$, the sum of the singleton set $\{r\}$ and the spectrum $\sigma(a)$ equals the spectrum of $\text{algebraMap}(r) + a$, i.e., $$ \{r\} + \sigma(a) = \sigma(\text{algebraMap}(r) + a). $$

spectrum.add_singleton_eq theorem

(a : A) (r : R) : σ a + { r } = σ (a + ↑ₐ r)

Full source

theorem add_singleton_eq (a : A) (r : R) : σ a + {r} = σ (a + ↑ₐ r) :=
  add_comm {r} (σ a) ▸ add_comm (algebraMap R A r) a ▸ singleton_add_eq a r

Spectrum Shift Identity: $\sigma(a) + \{r\} = \sigma(a + \text{algebraMap}(r))$

Informal description

Let $A$ be an algebra over a commutative ring $R$, and let $a \in A$. For any $r \in R$, the sum of the spectrum $\sigma(a)$ and the singleton set $\{r\}$ equals the spectrum of $a + \text{algebraMap}(r)$, i.e., $$ \sigma(a) + \{r\} = \sigma(a + \text{algebraMap}(r)). $$

spectrum.vadd_eq theorem

(a : A) (r : R) : r +ᵥ σ a = σ (↑ₐ r + a)

Full source

theorem vadd_eq (a : A) (r : R) : r +ᵥ σ a = σ (↑ₐ r + a) :=
  singleton_add.symm.trans <| singleton_add_eq a r

Spectrum Vector Addition Identity: $r +ᵥ \sigma(a) = \sigma(\text{algebraMap}(r) + a)$

Informal description

Let $A$ be an algebra over a commutative ring $R$, and let $a \in A$. For any $r \in R$, the vector addition of $r$ to the spectrum $\sigma(a)$ equals the spectrum of $\text{algebraMap}(r) + a$, i.e., $$ r +ᵥ \sigma(a) = \sigma(\text{algebraMap}(r) + a). $$

spectrum.neg_eq theorem

(a : A) : -σ a = σ (-a)

Full source

theorem neg_eq (a : A) : -σ a = σ (-a) :=
  Set.ext fun x => by
    simp only [mem_neg, mem_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]

Spectrum Negation Identity: $- \sigma(a) = \sigma(-a)$

Informal description

For any element $a$ in an $R$-algebra $A$, the negation of its spectrum equals the spectrum of its negation, i.e., $- \sigma(a) = \sigma(-a)$, where $\sigma(a)$ denotes the spectrum of $a$.

spectrum.singleton_sub_eq theorem

(a : A) (r : R) : { r } - σ a = σ (↑ₐ r - a)

Full source

theorem singleton_sub_eq (a : A) (r : R) : {r} - σ a = σ (↑ₐ r - a) := by
  rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]

Spectrum Subtraction Identity: $\{r\} - \sigma(a) = \sigma(\text{algebraMap}(r) - a)$

Informal description

Let $A$ be an algebra over a commutative ring $R$, and let $a \in A$. For any $r \in R$, the difference between the singleton set $\{r\}$ and the spectrum $\sigma(a)$ equals the spectrum of $\text{algebraMap}(r) - a$, i.e., $$ \{r\} - \sigma(a) = \sigma(\text{algebraMap}(r) - a). $$

spectrum.sub_singleton_eq theorem

(a : A) (r : R) : σ a - { r } = σ (a - ↑ₐ r)

Full source

theorem sub_singleton_eq (a : A) (r : R) : σ a - {r} = σ (a - ↑ₐ r) := by
  simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)

Spectrum Subtraction Identity: $\sigma(a) - \{r\} = \sigma(a - \text{algebraMap}(r))$

Informal description

Let $A$ be an algebra over a commutative ring $R$, and let $a \in A$. For any $r \in R$, the difference between the spectrum $\sigma(a)$ and the singleton set $\{r\}$ equals the spectrum of $a - \text{algebraMap}(r)$, i.e., $$ \sigma(a) - \{r\} = \sigma(a - \text{algebraMap}(r)). $$

spectrum.inv₀_mem_iff theorem

{r : R} {a : Aˣ} : r⁻¹ ∈ spectrum R (a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)

Full source

@[simp]
lemma inv₀_mem_iff {r : R} {a : Aˣ} :
    r⁻¹r⁻¹ ∈ spectrum R (a : A)r⁻¹ ∈ spectrum R (a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A) := by
  obtain (rfl | hr) := eq_or_ne r 0
  · simp [zero_mem_iff]
  · lift r to Rˣ using hr.isUnit
    simp [inv_mem_iff]

Spectrum Inversion Relation: $r^{-1} \in \sigma(a) \leftrightarrow r \in \sigma(a^{-1})$

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any unit $a$ in $A$ and any nonzero element $r \in R$, the inverse $r^{-1}$ belongs to the spectrum $\sigma(a)$ of $a$ if and only if $r$ belongs to the spectrum $\sigma(a^{-1})$ of the inverse $a^{-1}$.

spectrum.inv₀_mem_inv_iff theorem

{r : R} {a : Aˣ} : r⁻¹ ∈ spectrum R (↑a⁻¹ : A) ↔ r ∈ spectrum R (a : A)

Full source

lemma inv₀_mem_inv_iff {r : R} {a : Aˣ} :
    r⁻¹r⁻¹ ∈ spectrum R (↑a⁻¹ : A)r⁻¹ ∈ spectrum R (↑a⁻¹ : A) ↔ r ∈ spectrum R (a : A) := by
  simp

Spectrum Inversion Relation: $r^{-1} \in \sigma(a^{-1}) \leftrightarrow r \in \sigma(a)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any unit $a \in A^\times$ and any nonzero element $r \in R$, the multiplicative inverse $r^{-1}$ belongs to the spectrum of $a^{-1}$ if and only if $r$ belongs to the spectrum of $a$. In other words, $$ r^{-1} \in \sigma(a^{-1}) \leftrightarrow r \in \sigma(a). $$

spectrum.zero_eq theorem

[Nontrivial A] : σ (0 : A) = {0}

Full source

/-- Without the assumption `Nontrivial A`, then `0 : A` would be invertible. -/
@[simp]
theorem zero_eq [Nontrivial A] : σ (0 : A) = {0} := by
  refine Set.Subset.antisymm ?_ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])
  rw [spectrum, Set.compl_subset_comm]
  intro k hk
  rw [Set.mem_compl_singleton_iff] at hk
  have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
  simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]

Spectrum of Zero in a Nontrivial Algebra

Informal description

In a nontrivial algebra $A$ over a field $\mathbb{K}$, the spectrum of the zero element $0 \in A$ is the singleton set $\{0\}$, i.e., $\sigma(0) = \{0\}$.

spectrum.scalar_eq theorem

[Nontrivial A] (k : 𝕜) : σ (↑ₐ k) = { k }

Full source

@[simp]
theorem scalar_eq [Nontrivial A] (k : 𝕜) : σ (↑ₐ k) = {k} := by
  rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]

Spectrum of a Scalar in a Nontrivial Algebra: $\sigma(\text{algebraMap}(k)) = \{k\}$

Informal description

Let $A$ be a nontrivial algebra over a field $\mathbb{K}$. For any scalar $k \in \mathbb{K}$, the spectrum of the algebra homomorphism $\text{algebraMap}(k) \in A$ is the singleton set $\{k\}$, i.e., $$ \sigma(\text{algebraMap}(k)) = \{k\}. $$

spectrum.one_eq theorem

[Nontrivial A] : σ (1 : A) = { 1 }

Full source

@[simp]
theorem one_eq [Nontrivial A] : σ (1 : A) = {1} :=
  calc
    σ (1 : A) = σ (↑ₐ 1) := by rw [Algebra.algebraMap_eq_smul_one, one_smul]
    _ = {1} := scalar_eq 1

Spectrum of the Identity in a Nontrivial Algebra: $\sigma(1) = \{1\}$

Informal description

In a nontrivial algebra $A$ over a field $\mathbb{K}$, the spectrum of the multiplicative identity element $1 \in A$ is the singleton set $\{1\}$, i.e., $\sigma(1) = \{1\}$.

spectrum.smul_eq_smul theorem

[Nontrivial A] (k : 𝕜) (a : A) (ha : (σ a).Nonempty) : σ (k • a) = k • σ a

Full source

/-- the assumption `(σ a).Nonempty` is necessary and cannot be removed without
further conditions on the algebra `A` and scalar field `𝕜`. -/
theorem smul_eq_smul [Nontrivial A] (k : 𝕜) (a : A) (ha : (σ a).Nonempty) :
    σ (k • a) = k • σ a := by
  rcases eq_or_ne k 0 with (rfl | h)
  · simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)
  · exact unit_smul_eq_smul a (Units.mk0 k h)

Spectrum Scaling: $\sigma(k \cdot a) = k \cdot \sigma(a)$ for Nonempty Spectrum

Informal description

Let $A$ be a nontrivial algebra over a field $\mathbb{K}$. For any scalar $k \in \mathbb{K}$ and any element $a \in A$ with nonempty spectrum $\sigma(a)$, the spectrum of $k \cdot a$ equals $k$ multiplied by the spectrum of $a$, i.e., \[ \sigma(k \cdot a) = k \cdot \sigma(a). \]

spectrum.nonzero_mul_comm theorem

(a b : A) : σ (a * b) \ {0} = σ (b * a) \ {0}

Full source

theorem nonzero_mul_comm (a b : A) : σσ (a * b) \ {0} = σσ (b * a) \ {0} := by
  suffices h : ∀ x y : A, σσ (x * y) \ {0}σ (x * y) \ {0} ⊆ σ (y * x) \ {0} from
    Set.eq_of_subset_of_subset (h a b) (h b a)
  rintro _ _ k ⟨k_mem, k_neq⟩
  change ((Units.mk0 k k_neq) : 𝕜) ∈ _ at k_mem
  exact ⟨unit_mem_mul_comm.mp k_mem, k_neq⟩

Spectrum of Commuted Products: $\sigma(a * b) \setminus \{0\} = \sigma(b * a) \setminus \{0\}$

Informal description

For any elements $a$ and $b$ in an algebra $A$ over a commutative ring $R$, the nonzero elements of the spectrum of $a * b$ coincide with the nonzero elements of the spectrum of $b * a$. That is, $\sigma(a * b) \setminus \{0\} = \sigma(b * a) \setminus \{0\}$.

spectrum.map_inv theorem

(a : Aˣ) : (σ (a : A))⁻¹ = σ (↑a⁻¹ : A)

Full source

protected theorem map_inv (a : Aˣ) : (σ (a : A))⁻¹ = σ (↑a⁻¹ : A) := by
  refine Set.eq_of_subset_of_subset (fun k hk => ?_) fun k hk => ?_
  · rw [Set.mem_inv] at hk
    have : k ≠ 0 := by simpa only [inv_inv] using inv_ne_zero (ne_zero_of_mem_of_unit hk)
    lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr this
    rw [← Units.val_inv_eq_inv_val k] at hk
    exact inv_mem_iff.mp hk
  · lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr (ne_zero_of_mem_of_unit hk)
    simpa only [Units.val_inv_eq_inv_val] using inv_mem_iff.mp hk

Spectrum Inversion Identity: $(\sigma(a))^{-1} = \sigma(a^{-1})$ for units

Informal description

For any unit $a$ in an $R$-algebra $A$, the pointwise inverse of the spectrum $\sigma(a)$ equals the spectrum of the inverse element $a^{-1}$. That is, \[ (\sigma(a))^{-1} = \sigma(a^{-1}). \]

AlgHom.mem_resolventSet_apply theorem

(φ : F) {a : A} {r : R} (h : r ∈ resolventSet R a) : r ∈ resolventSet R ((φ : A → B) a)

Full source

theorem mem_resolventSet_apply (φ : F) {a : A} {r : R} (h : r ∈ resolventSet R a) :
    r ∈ resolventSet R ((φ : A → B) a) := by
  simpa only [map_sub, AlgHomClass.commutes] using h.map φ

Resolvent Set Preservation under Algebra Homomorphisms

Informal description

Let $R$ be a commutative semiring and $A$, $B$ be $R$-algebras. Given an $R$-algebra homomorphism $\varphi \colon A \to B$, an element $a \in A$, and $r \in R$ such that $r$ belongs to the resolvent set of $a$ (i.e., $\text{algebraMap}(r) - a$ is invertible in $A$), then $r$ also belongs to the resolvent set of $\varphi(a)$ in $B$.

AlgHom.spectrum_apply_subset theorem

(φ : F) (a : A) : σ ((φ : A → B) a) ⊆ σ a

Full source

theorem spectrum_apply_subset (φ : F) (a : A) : σσ ((φ : A → B) a) ⊆ σ a := fun _ =>
  mt (mem_resolventSet_apply φ)

Spectrum Inclusion under Algebra Homomorphisms: $\sigma(\varphi(a)) \subseteq \sigma(a)$

Informal description

Let $R$ be a commutative semiring and $A$, $B$ be $R$-algebras. For any $R$-algebra homomorphism $\varphi \colon A \to B$ and any element $a \in A$, the spectrum of $\varphi(a)$ is a subset of the spectrum of $a$, i.e., $\sigma(\varphi(a)) \subseteq \sigma(a)$.

AlgHom.apply_mem_spectrum theorem

[Nontrivial R] (φ : F) (a : A) : φ a ∈ σ a

Full source

theorem apply_mem_spectrum [Nontrivial R] (φ : F) (a : A) : φ a ∈ σ a := by
  have h : ↑ₐ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
    simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
      Algebra.id.map_eq_id, RingHom.id_apply, sub_self]
  simp only [spectrum.mem_iff, ← mem_nonunits_iff,
    coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]

Algebra Homomorphism Preserves Spectrum: $\varphi(a) \in \sigma(a)$

Informal description

Let $R$ be a nontrivial commutative semiring and $A$ be an $R$-algebra. For any algebra homomorphism $\varphi \colon A \to A$ and any element $a \in A$, the image $\varphi(a)$ belongs to the spectrum $\sigma(a)$ of $a$.

AlgEquiv.spectrum_eq theorem

 {F R A B : Type*} [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

Full source

@[simp]
theorem AlgEquiv.spectrum_eq {F R A B : Type*} [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 :=
  Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
    simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
      AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)

Spectrum Invariance under Algebra Isomorphism: $\sigma(f(a)) = \sigma(a)$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be rings equipped with $R$-algebra structures. Given an $R$-algebra isomorphism $f \colon A \to B$ (represented as an element of a type $F$ with `AlgEquivClass F R A B`), for any element $a \in A$, the spectrum of $f(a)$ in $B$ is equal to the spectrum of $a$ in $A$, i.e., \[ \sigma(f(a)) = \sigma(a). \]

spectrum.units_conjugate theorem

{a : A} {u : Aˣ} : spectrum R (u * a * u⁻¹) = spectrum R a

Full source

/-- Conjugation by a unit preserves the spectrum, inverse on right. -/
@[simp]
lemma spectrum.units_conjugate {a : A} {u : Aˣ} :
    spectrum R (u * a * u⁻¹) = spectrum R a := by
  suffices ∀ (b : A) (v : Aˣ), spectrumspectrum R (v * b * v⁻¹) ⊆ spectrum R b by
    refine le_antisymm (this a u) ?_
    apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
    simp [mul_assoc]
  intro a u μ hμ
  rw [spectrum.mem_iff] at hμ ⊢
  contrapose! hμ
  simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit

Spectrum Invariance under Conjugation by Units: $\sigma(u a u^{-1}) = \sigma(a)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any element $a \in A$ and any unit $u \in A^\times$, the spectrum of the conjugate element $u a u^{-1}$ is equal to the spectrum of $a$, i.e., \[ \sigma(u a u^{-1}) = \sigma(a). \]

spectrum.units_conjugate' theorem

{a : A} {u : Aˣ} : spectrum R (u⁻¹ * a * u) = spectrum R a

Full source

/-- Conjugation by a unit preserves the spectrum, inverse on left. -/
@[simp]
lemma spectrum.units_conjugate' {a : A} {u : Aˣ} :
    spectrum R (u⁻¹ * a * u) = spectrum R a := by
  simpa using spectrum.units_conjugate (u := u⁻¹)

Spectrum Invariance under Conjugation by Units (Inverse Form): $\sigma(u^{-1} a u) = \sigma(a)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any element $a \in A$ and any unit $u \in A^\times$, the spectrum of the conjugate element $u^{-1} a u$ is equal to the spectrum of $a$, i.e., \[ \sigma(u^{-1} a u) = \sigma(a). \]

Mathlib.Algebra.Algebra.Spectrum.Basic

Main definitions

Main statements

Notations