localization_comap_isInducing — Mathlib

English

The map comap induced by localization is an inducing map on spectra.

Русский

Отображение comap, индуцированное локализацией, является индуцирующим отображением между спектрами.

LaTeX

$$IsInducing (comap (algebraMap R S)).$$

Lean4

theorem localization_comap_isInducing [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    IsInducing (comap (algebraMap R S)) :=
  by
  refine ⟨TopologicalSpace.ext_isClosed fun Z ↦ ?_⟩
  simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus, @eq_comm _ _ (zeroLocus _), exists_exists_eq_and,
    preimage_comap_zeroLocus]
  constructor
  · rintro ⟨s, rfl⟩
    refine ⟨(Ideal.span s).comap (algebraMap R S), ?_⟩
    rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_comap M S]
  · rintro ⟨s, rfl⟩
    exact ⟨_, rfl⟩

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