quasispectrum_apply_subset — Mathlib

English

A simplified form of quasispectrum preservation under a non-unital algebra homomorphism, for rings where R is a commutative ring.

Русский

Упрощенная форма сохранения квазиспектра под действием неюнит-гомоморфизма алгебр, когда R — коммутативное кольцо.

LaTeX

$$$$ quasispectrum(R, φ(a)) \subseteq quasispectrum(R, a) $$$$

Lean4

/-- If `φ` is non-unital algebra homomorphism over a scalar ring `R`, then
`quasispectrum R (φ a) ⊆ quasispectrum R a`. -/
theorem quasispectrum_apply_subset {F R A B : Type*} [CommRing R] [NonUnitalRing A] [NonUnitalRing B] [Module R A]
    [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (a : A) :
    quasispectrum R (φ a) ⊆ quasispectrum R a :=
  NonUnitalAlgHom.quasispectrum_apply_subset' R φ a

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