Spec_fromSpecStalk — Mathlib

English

If X over Y is given, then the corresponding Spec.map stalk map has an IsOver structure by an instance, i.e., it is canonically over Y.

Русский

Если существует отображение X Over Y, то отображение stalkMap имеет структуру IsOver над Y по умолчанию.

LaTeX

$$instance [X.Over Y] {x} : Spec.map ((X ↘ Y).stalkMap x) |>.IsOver Y$$

Lean4

theorem Spec_fromSpecStalk (R : CommRingCat) (x) :
    (Spec R).fromSpecStalk x = Spec.map ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) := by
  rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial, IsAffineOpen.fromSpecStalk,
    IsAffineOpen.fromSpec_top, isoSpec_Spec_inv, ← Spec.map_comp]
    -- This is not a simp lemma to respect the abstraction boundaries

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