instIsEmptyCarrierCarrierCommRingCatSubschemeTop

Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop

English

The kernel of the map I.subschemeι.app U equals the ideal I(U).

Русский

Ядро отображения I.subschemeι.app U равно I(U).

LaTeX

$$$\ker\big(I.subschemeι.app U\big) = I.ideal U$$$

Lean4

instance : IsEmpty (⊤ : X.IdealSheafData).subscheme := by rw [← (subschemeι _).ker_eq_top_iff_isEmpty, ker_subschemeι]

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

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

Разделы

Аффилиация

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