fromSpecStalk_closedPoint — Mathlib

English

If x specializes to y, then the Spec map corresponding to stalk specialization yields an equality: Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x.

Русский

Если x специализируется на y, то выполняется равенство: Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x.

LaTeX

$$Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x$$

Lean4

@[simp]
theorem fromSpecStalk_closedPoint {x : X} : (X.fromSpecStalk x).base (closedPoint (X.presheaf.stalk x)) = x :=
  IsAffineOpen.fromSpecStalk_closedPoint _ _

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