Spec_fromSpecStalk' — Mathlib

English

A variant form of Spec_fromSpecStalk: for any R and x, (Spec R).fromSpecStalk x is equal to Spec.map (StructureSheaf.toStalk R _) .

Русский

Вариант формы Spec_fromSpecStalk: для любого кольца R и точки x, fromSpecStalk x равен Spec.map (StructureSheaf.toStalk R _).

LaTeX

$$Spec.fromSpecStalk' (R) (x) = Spec.map (StructureSheaf.toStalk R _)$$

Lean4

/-- A variant of `Spec_fromSpecStalk` that breaks abstraction boundaries. -/
theorem Spec_fromSpecStalk' (R : CommRingCat) (x) : (Spec R).fromSpecStalk x = Spec.map (StructureSheaf.toStalk R _) :=
  Spec_fromSpecStalk _ _

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