subscheme

Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

Lean4

/-- The subscheme associated to an ideal sheaf. -/
noncomputable def subscheme : Scheme :=
  I.glueData.glued.restrict (f := TopCat.ofHom (toContinuousMap I.gluedHomeo.symm)) I.gluedHomeo.symm.isOpenEmbedding

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

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

Разделы

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

Аффилиация

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