Γ_map_op — Mathlib

English

Let X and Y be Locally Ringed Spaces and f: X → Y a morphism. The map on global sections induced by f, viewed in the opposite direction, coincides with the component of f at the top open. In symbols, Γ.map f.op = f.c.app (op ⊤).

Русский

Пусть X и Y — локальноокружённые пространства, f: X → Y — гомоморфизм. Отображение на глобальные секции, получаемое из f через противоположное направление, совпадает с компонентой гомоморфизма f на верхнем открытом множестве. Другими словами, Γ.map f.op = f.c.app (op ⊤).

LaTeX

$$$$\\Gamma.map f^{op} = f.c.app (\\mathrm{op}\\,\\top)$$$$

Lean4

theorem Γ_map_op {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) : Γ.map f.op = f.c.app (op ⊤) :=
  rfl

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