instIsOverMapStalkMapOverInferInstanceOverClass

English

If X over Y then the stalk map induces an over morphism in the Spec category; in particular, the map Spec.map (X.Hom.stalkMap x) yields an IsOver morphism over Y.

Русский

Если X над Y, то stalkMap порождает отображение над Y в категории Spec; т.е. Spec.map(stalkMap x) образует IsOver по Y.

LaTeX

$$Spec.map (X.Hom.stalkMap x) IsOver Y$$

Lean4

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

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