English
For any R, the top-level morphism of the SpecIso between A(n; R) and Spec R is given by the composite of ΓSpecIso, evaluation on coordinates, and the canonical maps; i.e., the appTop component is computable by the explicit formula shown.
Русский
Для любого кольца R верхний компонент морфизма SpecIso между 𝔸(n; R) и Spec R задается явным образом через ΓSpecIso и координаты.
LaTeX
$$$(\\mathrm{SpecIso}\\; n\\; R).\\mathrm{hom}.\\mathrm{appTop} = (\\mathrm{Scheme.}\\Gamma\\mathrm{SpecIso}(_)).\\mathrm{hom} \\circ \\mathrm{ofHom}(\\mathrm{eval}_2\\mathrm{Hom}(\\cdots).\\mathrm{hom}(\\mathrm{coord}(\\mathrm{Spec} \\; R))).$$$
Lean4
@[simp]
theorem SpecIso_hom_appTop (R : CommRingCat.{max u v}) :
(SpecIso n R).hom.appTop =
(Scheme.ΓSpecIso _).hom ≫
CommRingCat.ofHom (eval₂Hom ((Scheme.ΓSpecIso _).inv ≫ (𝔸(n; Spec R) ↘ Spec R).appTop).hom (coord (Spec R))) :=
by
simp only [SpecIso, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map, Quiver.Hom.unop_op,
TopologicalSpace.Opens.map_top, Scheme.comp_app, isoOfIsAffine_hom_appTop, Scheme.ΓSpecIso_naturality_assoc]
congr 1
ext : 1
apply ringHom_ext'
· ext; simp
· simp
