isoOfIsAffine_hom_appTop — Mathlib

English

For an affine base S, the inverse of the isomorphism isoOfIsAffine intertwines the coordinate functions with the corresponding X_i coordinates on Spec; in particular applying inv to appTop(coord i) yields the corresponding coordinate on the spectrum.

Русский

Для аффинной базы S обратный изоморфизма isoOfIsAffine переводит координаты соответствующим образом: применение inv к appTop(coord i) возвращает координату на спектре.

LaTeX

$$$(\\mathrm{isoOfIsAffine}\\; n\\; S)^{-1} \\circ \\mathrm{coord}_S(i) = \\mathrm{coord}_{\\mathrm{Spec}}(i).$$$

Lean4

@[simp]
theorem isoOfIsAffine_hom_appTop [IsAffine S] :
    (isoOfIsAffine n S).hom.appTop =
      (Scheme.ΓSpecIso _).hom ≫ CommRingCat.ofHom (eval₂Hom ((𝔸(n; S) ↘ S).appTop).hom (coord S)) :=
  by simp [isoOfIsAffine_hom]

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