fromSpec_primeIdealOf — Mathlib

English

The prime ideal corresponding to a point in U, when viewed via the Spec map from X, maps back to the point in U under the overall structure map.

Русский

Прайм-идеал, соответствующий точке в U, при отображении через отображение Spec обратно восстанавливает саму точку в U под общей структурной карте.

LaTeX

$$$h_U.\text{primeIdealOf}(x) = (\text{Spec.map} (X.presheaf.germ\_x)).base(\text{closedPoint})$$$

Lean4

theorem fromSpec_primeIdealOf (x : U) : hU.fromSpec.base (hU.primeIdealOf x) = x.1 :=
  by
  dsimp only [IsAffineOpen.fromSpec, Subtype.coe_mk, IsAffineOpen.primeIdealOf]
  rw [← Scheme.comp_base_apply, Iso.hom_inv_id_assoc]
  rfl

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