localizationToStalk_stalkToFiberRingHom

Mathlib.AlgebraicGeometry.StructureSheaf

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

← MathLib Explorer

English

The stalk-to-fiber morphism is an isomorphism, hence invertible on carriers.

Русский

Морфизм stalk-to-fiber изоморфен и обратим на носителях.

LaTeX

$$$(stalkToFiberRingHom\\; R\\; x)$ is an isomorphism of rings.$$

Lean4

@[simp, reassoc]
theorem localizationToStalk_stalkToFiberRingHom (x : PrimeSpectrum.Top R) :
    localizationToStalk R x ≫ stalkToFiberRingHom R x = 𝟙 _ :=
  (stalkIso R x).inv_hom_id

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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