instIsIsoCommRingCatStalkToFiberRingHom

Mathlib.AlgebraicGeometry.StructureSheaf

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.StructureSheaf.instIsIsoCommRingCatStalkToFiberRingHom

English

For any R and any prime x, the map stalkToFiberRingHom R x is an isomorphism.

Русский

Для любого кольца R и любой простоты x отображение stalkToFiberRingHom R x является изоморфизмом.

LaTeX

$$$stalkToFiberRingHom(R, x) \\text{ is an isomorphism.}$$$

Lean4

instance (x : PrimeSpectrum R) : IsIso (stalkToFiberRingHom R x) :=
  (stalkIso R x).isIso_hom

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru