instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat

← MathLib Explorer

English

If X is a compact space, then X.toSpecΓ is dominant.

Русский

Если X компактно, то отображение X to Spec Γ(X, ⊤) доминантно.

LaTeX

$$$[CompactSpace X] \\Rightarrow IsDominant(X.toSpecΓ)$$$

Lean4

instance [CompactSpace X] : IsDominant X.toSpecΓ :=
  isDominant_of_of_appTop_injective
    (by simpa only [Scheme.toSpecΓ_appTop] using (ConcreteCategory.bijective_of_isIso (Scheme.ΓSpecIso Γ(X, ⊤)).hom).1)

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

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

Разделы

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

Аффилиация

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