instIsAffineHomOverSchemeInferInstanceOverClass

Mathlib.AlgebraicGeometry.AffineSpace

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

English

If n is finite, the morphism 𝔸(n; S) ↓ S is an affine morphism of schemes (in the over-S category).

Русский

Если n конечен, морфизм 𝔸(n; S) ↓ S является аффинным морфизмом схем (в категории над S).

LaTeX

$$$[Finite\\ n]\\Rightarrow IsAffineHom\\big(\\mathbb{A}(n; S) \\downarrow S\\big).$$$

Lean4

instance : IsAffineHom (𝔸(n; S) ↘ S) :=
  MorphismProperty.pullback_fst _ _ inferInstance

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

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

Разделы

Аффилиация

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