not_isIntegralHom

Mathlib.AlgebraicGeometry.AffineSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineSpace.not_isIntegralHom

English

If S and n are both nonempty, then the morphism 𝔸(n; S) ↓ S is not integral.

Русский

Если S и n оба непусты, то 𝔸(n; S) ↓ S не является интегральным.

LaTeX

$$$[\text{Nonempty } S] \land [\text{Nonempty } n] \Rightarrow \neg IsIntegralHom(\mathbb{A}(n;S) \downarrow S)$$$

Lean4

theorem not_isIntegralHom [Nonempty S] [Nonempty n] : ¬IsIntegralHom (𝔸(n; S) ↘ S) := by
  simp [isIntegralHom_over_iff_isEmpty]

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

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

Разделы

Аффилиация

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