toToΓSpecMapBasicOpen — Mathlib

English

The unit map for the basic open induces a unit on the corresponding localization maps, reflecting invertibility locally.

Русский

Единичный элемент в локализации отображает локальную инвертируемость на базовом открытом.

LaTeX

$$$X.toToΓSpecMapBasicOpen(r) \text{ is a unit in the corresponding localization.}$$$

Lean4

/-- The map from the global sections `Γ(X)` to the sections on the (preimage of) a basic open. -/
abbrev toToΓSpecMapBasicOpen : X.presheaf.obj (op ⊤) ⟶ X.presheaf.obj (op <| X.toΓSpecMapBasicOpen r) :=
  X.presheaf.map (X.toΓSpecMapBasicOpen r).leTop.op

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