English
There is a homeomorphism between the spectrum of a with respect to S and the spectrum with respect to R induced by SpectrumRestricts a f.
Русский
Существует гомеоморфизм между спектрами элемента a в рамках S и R, индуцируемый SpectrumRestricts a f.
LaTeX
$$$\\text{SpectrumRestricts\\,homeomorph}: \\mathrm{spectrum}\\;S\\;a \\cong_{\\mathrm{top}} \\mathrm{spectrum}\\;R\\;a$$$
Lean4
/-- The homeomorphism `spectrum S a ≃ₜ spectrum R a` induced by `SpectrumRestricts a f`. -/
def homeomorph {R S A : Type*} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A]
[IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] [ContinuousSMul R S] {a : A} {f : C(S, R)}
(h : SpectrumRestricts a f) : spectrum S a ≃ₜ spectrum 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
