isStableUnderBaseChange

Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange

English

Every mono morphism of schemes is UniversallyInjective.

Русский

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

LaTeX

$$$\forall f,\; \text{Mono}(f) \Rightarrow \operatorname{UniversallyInjective}(f).$$$

Lean4

instance isStableUnderBaseChange : IsStableUnderBaseChange @UniversallyInjective :=
  universallyInjective_eq_diagonal.symm ▸ inferInstance

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

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

Разделы

Аффилиация

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