imageOfDf_eq_comap_C_compl_zeroLocus

English

The map on spectra induced by comap with polynomial constants is an open map.

Русский

Отображение спектра, индуцированное comap C, является открытым отображением.

LaTeX

$$$IsOpenMap(\\operatorname{PrimeSpectrum.comap}(C))$$$

Lean4

/-- The open set `imageOfDf f` coincides with the image of `basicOpen f` under the
morphism `C⁺ : Spec R[x] → Spec R`. -/
theorem imageOfDf_eq_comap_C_compl_zeroLocus :
    imageOfDf f = PrimeSpectrum.comap (C : R →+* R[X]) '' (zeroLocus { f })ᶜ :=
  by
  ext x
  refine ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime x.isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩
  · rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]
    obtain ⟨i, hi⟩ := hx
    exact fun a => hi (mem_map_C_iff.mp a i)
  · ext x
    refine ⟨fun h => ?_, fun h => subset_span (mem_image_of_mem C.1 h)⟩
    rw [← @coeff_C_zero R x _]
    exact mem_map_C_iff.mp h 0
  · rintro ⟨xli, complement, rfl⟩
    exact comap_C_mem_imageOfDf complement

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