range_fromSpecStalk — Mathlib

English

As before, the range of the base map of X.fromSpecStalk x equals the specialization set { y | y ⤳ x }. This identifies the image of the stalk map with the specialization relation.

Русский

Как и ранее, образ базового отображения fromSpecStalk равен множеству точек, специализирующихся на x.

LaTeX

$$Set.range (X.fromSpecStalk x).base = {y | y ⤳ x}$$

Lean4

@[stacks 01J7]
theorem range_fromSpecStalk {x : X} : Set.range (X.fromSpecStalk x).base = {y | y ⤳ x} :=
  by
  ext y
  constructor
  · rintro ⟨y, rfl⟩
    exact
      ((IsLocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).base.hom.2).trans
        (specializes_of_eq fromSpecStalk_closedPoint)
  · rintro (hy : y ⤳ x)
    have := fromSpecStalk_closedPoint (x := y)
    rw [← Spec_map_stalkSpecializes_fromSpecStalk hy] at this
    exact ⟨_, this⟩

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