instOfIsOpenImmersion

Mathlib.AlgebraicGeometry.Morphisms.Immersion

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

← MathLib Explorer

English

The equalizer immersion equalizer.ι f g is immersion for any morphisms f,g.

Русский

Неравноймерная вложение equalizer.ι f g является вложением для любых f,g.

LaTeX

$$$\\text{IsImmersion}(\\text{equalizer.ι}(f,g))$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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