instIsOverMapResidueFieldMapOverInferInstanceOverClass

Mathlib.AlgebraicGeometry.ResidueField

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass

English

If X over Y, then the morphism on residue-field maps arising from a point x is over Y.

Русский

Если X над Y, то отображение остаточных полей, получаемое для точки x, является over-морфизмом над Y.

LaTeX

$$∀ x, IsOver (X.residueFieldMap (over X Y inferInstance) x) Y$$

Lean4

instance [X.Over Y] (x : X) : Spec.map ((X ↘ Y).residueFieldMap x) |>.IsOver Y where

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

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

Разделы

Аффилиация

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