English
For φ: R → S, map n (Spec.map φ) decomposes as a composite involving SpecIso and a polynomial map; i.e., a natural transformation through SpecIso and Spec.map of MvPolynomial.map φ.hom.
Русский
Для φ: R → S отображение map n (Spec.map φ) раскладывается на композицию через SpecIso и полиномную карту; естественное преобразование через SpecIso и Spec.map(MvPolynomial.map φ.hom).
LaTeX
$$$map\\ n\\ (\\mathrm{Spec.map}\\ φ) = (SpecIso\\ n\\; S).hom \\circ \\mathrm{Spec.map}(\\mathrm{ofHom}(\\mathrm{MvPolynomial.map}(φ.hom))) \\circ (\\mathrm{SpecIso}\\ n\\; R).inv$$$
Lean4
theorem map_Spec_map {R S : CommRingCat.{max u v}} (φ : R ⟶ S) :
map n (Spec.map φ) =
(SpecIso n S).hom ≫ Spec.map (CommRingCat.ofHom (MvPolynomial.map φ.hom)) ≫ (SpecIso n R).inv :=
by
rw [← Iso.inv_comp_eq]
ext1
· simp only [map_over, Category.assoc, SpecIso_inv_over, SpecIso_inv_over_assoc, ← Spec.map_comp,
← CommRingCat.ofHom_comp]
rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom]
· simp only [TopologicalSpace.Opens.map_top, Scheme.comp_app, CommRingCat.comp_apply]
conv_lhs => enter [2]; tactic => exact map_appTop_coord _ _
conv_rhs => enter [2]; tactic => exact SpecIso_inv_appTop_coord _ _
rw [SpecIso_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality, CommRingCat.comp_apply,
ConcreteCategory.hom_ofHom, map_X]
