English
For R and i ∈ n, the inverse SpecIso applied to coord_i gives the X_i coordinate under ΓSpecIso; i.e., the inverse sends the coordinate function to the corresponding X_i on Spec R.
Русский
Для R и i ∈ n обратный SpecIso отправляет coord_i в X_i через ΓSpecIso; то есть обратное отображение отправляет координатную функцию в соответствующую X_i на Spec R.
LaTeX
$$$(\\mathrm{SpecIso}\\; n\\; R)^{-1}.\\mathrm{appTop}(\\mathrm{coord}_S(i)) = (\\mathrm{Scheme.}\\Gamma\\mathrm{SpecIso}(.{\\rm of} _)).inv(\\mathrm{X}_i).$$$
Lean4
@[simp]
theorem SpecIso_inv_appTop_coord (R : CommRingCat.{max u v}) (i) :
(SpecIso n R).inv.appTop (coord _ i) = (Scheme.ΓSpecIso (.of _)).inv (.X i) :=
by
simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, Scheme.Spec_map, Quiver.Hom.unop_op,
TopologicalSpace.Opens.map_top, Scheme.comp_app, CommRingCat.comp_apply]
rw [isoOfIsAffine_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
CommRingCat.comp_apply]
congr 1
exact map_X _ _
