English
There is a natural homeomorphism between the quasispectrum of a over S and the quasispectrum over R induced by restriction via f.
Русский
Существует естественная гомеоморфизма между квази-спектром S(a) и квази-спектром R(a), индуцированного ограничением через f.
LaTeX
$$$\\sigma_n(S,a) \\cong_t \\sigma_n(R,a)$$$
Lean4
/-- The homeomorphism `quasispectrum S a ≃ₜ quasispectrum R a` induced by
`QuasispectrumRestricts a f`. -/
def homeomorph {R S A : Type*} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module R A] [Module S A]
[IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] [ContinuousSMul R S] [IsScalarTower S A A]
[SMulCommClass S A A] {a : A} {f : C(S, R)} (h : QuasispectrumRestricts a f) : σₙ S a ≃ₜ σₙ R a
where
toFun := MapsTo.restrict f _ _ h.subset_preimage
invFun := MapsTo.restrict (algebraMap R S) _ _ (image_subset_iff.mp h.algebraMap_image.subset)
left_inv x := Subtype.ext <| h.rightInvOn x.2
right_inv x := Subtype.ext <| h.left_inv x
continuous_toFun := continuous_induced_rng.mpr <| f.continuous.comp continuous_induced_dom
continuous_invFun := continuous_induced_rng.mpr <| continuous_algebraMap R S |>.comp continuous_induced_dom
