pointsPi_surjective_of_isAffine — Mathlib

English

If X is affine, then the natural map pointsPi from the product of Spec-type rings to X is surjective; equivalently, every point of X lies in the image of pointsPi.

Русский

Если X аффинный, то естественная карта pointsPi есть сюръективна; то есть каждый пункт пространства X лежит в образе pointsPi.

LaTeX

$$$\\operatorname{Surjective}(\\mathrm{pointsPi}\\ R\\ X)$$$

Lean4

theorem pointsPi_surjective_of_isAffine [IsAffine X] : Function.Surjective (pointsPi R X) :=
  by
  rintro f
  refine ⟨Spec.map (CommRingCat.ofHom (Pi.ringHom fun i ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).1)) ≫ X.isoSpec.inv, ?_⟩
  ext i : 1
  simp only [pointsPi, ← Spec.map_comp_assoc, Iso.comp_inv_eq]
  exact Spec.map_preimage _

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