toSet_map — Mathlib

English

Let f be a ring homomorphism and s a constructible data over R. Then the underlying set of the constructible data obtained by pushing forward along f equals the preimage of s under the induced map on spectra; i.e., the two sets in Spec S and Spec R correspond via comap f.

Русский

Пусть f — гомоморфизм колец и s — конструктивное множество над R. Тогда множество, связанное с образованным по f конструктивным набором, совпадает с предобразом множества s по отображению спектра, индуцированному f; то есть существует соответствие через знакомство comap f.

LaTeX

$$$ (s.map f)^{\mathrm{toSet}} = \mathrm{comap}(f)^{-1}(s^{\mathrm{toSet}}) $$$

Lean4

@[simp]
theorem toSet_map (f : R →+* S) (s : ConstructibleSetData R) : (s.map f).toSet = comap f ⁻¹' s.toSet :=
  by
  unfold toSet map
  rw [set_biUnion_finset_image]
  simp

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