instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral

Mathlib.AlgebraicGeometry.FunctionField

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral

← MathLib Explorer

English

If X is integral and x ∈ X, the stalk O_{X,x} is a domain.

Русский

Если X целый и x ∈ X, то локальный стержень O_{X,x} является доменом.

LaTeX

$$$[\operatorname{IsIntegral} X]\Rightarrow \operatorname{IsDomain}(X.presheaf.stalk x).carrier.$$$

Lean4

instance [IsIntegral X] {x : X} : IsDomain (X.presheaf.stalk x) :=
  Function.Injective.isDomain _ (IsFractionRing.injective (X.presheaf.stalk x) (X.functionField))

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

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

Разделы

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

Аффилиация

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