appTop — Mathlib

English

The appTop map is the induced map on global sections for the top open, i.e., the restriction map on global sections for the largest open subset.

Русский

appTop задаёт индукированное отображение на глобальные секции для верхнего открытия, то есть ограничение на самой большой открытой подстановке.

LaTeX

$$$\mathrm{appTop} : \Gamma(Y,\top) \to \Gamma(X,\top)$$$

Lean4

/-- Given a morphism of schemes `f : X ⟶ Y`,
this is the induced map `Γ(Y, ⊤) ⟶ Γ(X, ⊤)`. -/
abbrev appTop : Γ(Y, ⊤) ⟶ Γ(X, ⊤) :=
  f.app ⊤

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