instOfIsClosedImmersion

Mathlib.AlgebraicGeometry.Morphisms.Immersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsImmersion.instOfIsClosedImmersion

← MathLib Explorer

English

If f is an immersion, then the natural map f.toImage is an immersion.

Русский

Если f — вложение, то отображение f.toImage также является вложением.

LaTeX

$$$\\text{IsImmersion}(f.toImage)$$$

Lean4

instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : IsImmersion f where
  isLocallyClosed_range := f.isClosedEmbedding.2.isLocallyClosed

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

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

Разделы

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

Аффилиация

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