le_monomorphisms

Mathlib.AlgebraicGeometry.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsOpenImmersion.le_monomorphisms

← MathLib Explorer

English

Every open immersion is a mono morphism in the scheme category.

Русский

Каждое открытое вложение является моно-морфизмом в категории схем.

LaTeX

$$$\forall f, \text{IsOpenImmersion}(f) \Rightarrow \text{Mono}(f)$$$

Lean4

theorem le_monomorphisms : IsOpenImmersion ≤ MorphismProperty.monomorphisms Scheme.{u} := fun _ _ _ _ ↦
  MorphismProperty.monomorphisms.infer_property _

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

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

Разделы

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

Аффилиация

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