fromSpec_image_basicOpen — Mathlib

English

The image of a prime basic open under fromSpec is the basic open of the underlying basic open on X.

Русский

Образ базовой открытой области под fromSpec равен базовой открытой области на X.

LaTeX

$$$\mathrm{h_U.fromSpec} ''^U (\mathrm{PrimeSpectrum.basicOpen} f) = X.basicOpen f$$$

Lean4

theorem fromSpec_image_basicOpen : hU.fromSpec ''ᵁ (PrimeSpectrum.basicOpen f) = X.basicOpen f :=
  by
  rw [← hU.fromSpec_preimage_basicOpen]
  ext1
  change hU.fromSpec.base '' (hU.fromSpec.base ⁻¹' (X.basicOpen f : Set X)) = _
  rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, hU.range_fromSpec]
  exact Scheme.basicOpen_le _ _

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