arrowIsoSpecΓOfIsAffine — Mathlib

English

If f: X → Y is a morphism of affine schemes, the arrow f is isomorphic to the arrow induced by the map on global sections on Spec.

Русский

Если f: X → Y — морфизм аффинных схем, то стрелка f изоморфна стрелке, полученной от маппинга по глобальным секциям на Spec.

LaTeX

$$$\\text{Arrow.mk}(f) \\cong \\text{Arrow.mk}(\\mathrm{Spec.map}(f.\\mathrm{appTop}))$$$

Lean4

/-- If `f : X ⟶ Y` is a morphism between affine schemes, the corresponding arrow is isomorphic
to the arrow of the morphism on prime spectra induced by the map on global sections. -/
noncomputable def arrowIsoSpecΓOfIsAffine {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
    Arrow.mk f ≅ Arrow.mk (Spec.map f.appTop) :=
  Arrow.isoMk X.isoSpec Y.isoSpec (ΓSpec.adjunction.unit_naturality _)

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