toSpec — Mathlib

English

There is a natural morphism from Proj|D(f) to Spec A⁰_f induced by the canonical ring map A⁰_f → Γ(Proj, D(f)).

Русский

Существует естественный морфизм из Proj|D(f) в Spec A⁰_f, вызываемый каноническим кольцевым отображением A⁰_f → Γ(Proj, D(f)).

LaTeX

$$$\\text{toSpec}(f) : (Proj| pbo f) ⟶ \\mathrm{Spec}(A⁰_f)$$$

Lean4

/-- The morphism of locally ringed space from `Proj|D(f)` to `Spec A⁰_f` induced by the ring map
`A⁰_ f → Γ(Proj, D(f))` under the gamma spec adjunction.
-/
def toSpec (f) : (Proj| pbo f) ⟶ Spec (A⁰_ f) :=
  ΓSpec.locallyRingedSpaceAdjunction.homEquiv (Proj| pbo f) (op (CommRingCat.of <| A⁰_ f)) (awayToΓ 𝒜 f).op

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