instIsOverHomOfVectorOverSchemeInferInstanceOverClass

English

Let X be a scheme over S. For every n and every n-tuple of global sections v ∈ Γ(X, 𝒪_X)^n, the induced morphism homOfVector(X ↓ S, v): X → 𝔸(n; S) is over S (i.e., its composition with the projection 𝔸(n; S) → S equals the structural morphism X → S).

Русский

Пусть X — схема над S. Пусть n — тип, и возьмем любой n-uple глобальных секций v ∈ Γ(X, 𝒪_X)^n. Тогда полученный из v морфизм homOfVector(X ↓ S, v): X → 𝔸(n; S) является над S (то есть композиция с проекцией 𝔸(n; S) → S дает структурный морфизм X → S).

LaTeX

$$$\\forall v \\in \\Gamma(X, \\mathcal{O}_X)^n:\\; \\operatorname{IsOver}_S\\big(\\operatorname{homOfVector}(X \\downarrow S, v)\\big).$$$

Lean4

instance (v : n → Γ(X, ⊤)) : (homOfVector (X ↘ S) v).IsOver S where

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