arrowIsoΓSpecOfIsAffine — Mathlib

English

For affine X,Y and morphism f: X → Y, the arrow f corresponds to the map on prime spectra induced by f.appTop.

Русский

Для аффинных X,Y и морфизма f: X → Y стрелка f соответствует стрелке на спектрах, индукцируемой f.appTop.

LaTeX

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

Lean4

/-- If `f : A ⟶ B` is a ring homomorphism, the corresponding arrow is isomorphic
to the arrow of the morphism induced on global sections by the map on prime spectra. -/
def arrowIsoΓSpecOfIsAffine {A B : CommRingCat} (f : A ⟶ B) : Arrow.mk f ≅ Arrow.mk ((Spec.map f).appTop) :=
  Arrow.isoMk (Scheme.ΓSpecIso _).symm (Scheme.ΓSpecIso _).symm (Scheme.ΓSpecIso_inv_naturality f).symm

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