stalkAlgebra_map — Mathlib

English

Explicit description of toBasicOpen on a mk' fraction aligns with the corresponding constant section on basicOpen g.

Русский

Явное описание toBasicOpen на дроби mk' согласуется с соответствующей константной секцией на базовом открытом g.

LaTeX

$$$toBasicOpen(R,f) (IsLocalization.mk'(Localization.Away f, a, b)) = const(R, a, f, \\operatorname{basicOpen} f)\\; (with\\; proper\\; identifications)$$$

Lean4

@[simp]
theorem stalkAlgebra_map (p : PrimeSpectrum R) (r : R) :
    algebraMap R ((structureSheaf R).presheaf.stalk p) r = toStalk R p r :=
  rfl

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