algebraMap_image — Mathlib

English

If SpectrumRestricts a f, then the image of spectrum R a under algebraMap R S equals spectrum S a.

Русский

Если SpectrumRestricts a f, то образ спектра R a под алгебраMap R S равен спектру S a.

LaTeX

$$$ \\mathrm{algebraMap}_{R S}''\\mathrm{spectrum} R a = \\mathrm{spectrum} S a $$$

Lean4

theorem algebraMap_image (h : SpectrumRestricts a f) : algebraMap R S '' spectrum R a = spectrum S a :=
  by
  refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
  · simpa only [spectrum.preimage_algebraMap] using (spectrum S a).image_preimage_subset (algebraMap R S)
  exact ⟨spectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

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