English
The inverse of SpecIso n R followed by the morphism to Spec R equals the canonical Spec.map from the polynomial coordinate ring; i.e., SpecIso inv composed with the base projection recovers Spec.map on coefficients.
Русский
Обратный SpecIso после применения к Spec R восстанавливает стандартное отображение Spec.map на коэффициентах полиномов.
LaTeX
$$$(\\mathrm{SpecIso}\\; n\\; R)^{-1} \\circ 𝔸(n; \\mathrm{Spec} R) \\downarrow \\mathrm{Spec} R = \\mathrm{Spec.map}(\\mathrm{ofHom} \\ C).$$$
Lean4
@[reassoc (attr := simp)]
theorem SpecIso_inv_over (R : CommRingCat.{max u v}) :
(SpecIso n R).inv ≫ 𝔸(n; Spec R) ↘ Spec R = Spec.map (CommRingCat.ofHom C) :=
by
simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, Scheme.Spec_map, Quiver.Hom.unop_op,
Category.assoc, isoOfIsAffine_inv_over, Scheme.isoSpec_Spec_inv, ← Spec.map_comp]
congr 1
rw [Iso.inv_comp_eq]
ext : 2
exact map_C _ _
