appLE — Mathlib

English

The app map is the induced map on global sections from Y to X for a morphism f: X → Y, expressed via the presheaf maps on the structure sheaves.

Русский

отображение app есть индуцированное отображение глобальных секций от Y к X для морфизма f: X → Y, задаётся через отображения прешфейза на структурных оболочках.

LaTeX

$$$\mathrm{app}(f,U) : \Gamma(Y,U) \to \Gamma(X,f^{-1}(U))$$$

Lean4

/-- Given a morphism of schemes `f : X ⟶ Y`, and open sets `U ⊆ Y`, `V ⊆ f ⁻¹' U`,
this is the induced map `Γ(Y, U) ⟶ Γ(X, V)`. -/
def appLE (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U) : Γ(Y, U) ⟶ Γ(X, V) :=
  f.app U ≫ X.presheaf.map (homOfLE e).op

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