subset_subalgebra — Mathlib

English

Let S be a subalgebra of A. For a ∈ S, the spectrum computed in A is contained in the spectrum computed in S: spectrum_R(a) ⊆ spectrum_R^S(a).

Русский

Пусть S — подалгебра A. Для a ∈ S спектр, взятый в A, содержится в спектре, взятом в S: σ_R^A(a) ⊆ σ_R^S(a).

LaTeX

$$$\sigma_R(a) \subseteq \sigma_R^{S}(a)$$$

Lean4

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) : spectrum R (a : A) ⊆ spectrum R a :=
  Set.compl_subset_compl.mpr fun _ ↦ IsUnit.map (SubalgebraClass.val s)

Похожие утверждения