resLE — Mathlib

English

Let f: X → Y be a morphism of schemes. For open sets U ⊆ Y and V ⊆ X with V contained in the preimage f^{-1}(U), the restriction of f to U defines a morphism from V to U, given by composing the canonical map X.homOfLE with the restriction f|_U.

Русский

Пусть f: X → Y — морфизм схем. Для открытых множеств U ⊆ Y и V ⊆ X с V ⊆ f^{-1}(U) ограничение f на U задаёт морфизм V → U, который получается как композиция X.homOfLE с ограничением f|_U.

LaTeX

$$$\mathrm{resLE}(f,U,V,e) = X.homOfLE(e) \circ f|_U$$$

Lean4

/-- The restriction of a morphism `f : X ⟶ Y` to open sets on the source and target. -/
def resLE (f : Hom X Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U) : V.toScheme ⟶ U.toScheme :=
  X.homOfLE e ≫ f ∣_ U

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