English
If S is an affine scheme, then the affine space over S is canonically isomorphic to the spectrum of the polynomial ring in n variables over Γ(S, 𝒪_S); namely 𝔸(n; S) ≅ Spec Γ(S, 𝒪_S)[x_1,...,x_n].
Русский
Если S — аффинная схема, то аффинное пространство над S канонически изоморфно спектру многочленного кольца по n переменным над Γ(S, 𝒪_S); то есть 𝔸(n; S) ≅ Spec Γ(S, 𝒪_S)[x_1,...,x_n].
LaTeX
$$$[IsAffine\\ S] \\Rightarrow \\mathbb{A}(n; S) \\cong \\mathrm{Spec}\\big(\\mathrm{MvPolynomial}_n(\\Gamma(S, \\mathcal{O}_S))\\big).$$$
Lean4
/-- The affine space over an affine base is isomorphic to the spectrum of the polynomial ring.
Also see `AffineSpace.SpecIso`.
-/
@[simps -isSimp hom inv]
def isoOfIsAffine [IsAffine S] : 𝔸(n; S) ≅ Spec <| .of <| MvPolynomial n Γ(S, ⊤)
where
hom := 𝔸(n; S).toSpecΓ ≫ Spec.map (CommRingCat.ofHom (eval₂Hom ((𝔸(n; S) ↘ S).appTop).hom (coord S)))
inv :=
homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
((Scheme.ΓSpecIso (.of (MvPolynomial n Γ(S, ⊤)))).inv ∘ MvPolynomial.X)
hom_inv_id := by
ext1
· simp only [Category.assoc, homOfVector_over, Category.id_comp]
rw [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, eval₂Hom_comp_C, CommRingCat.ofHom_hom, ←
Scheme.toSpecΓ_naturality_assoc]
simp [Scheme.isoSpec]
· simp only [Category.assoc, Scheme.comp_app, Scheme.comp_coeBase, TopologicalSpace.Opens.map_comp_obj,
TopologicalSpace.Opens.map_top, Scheme.toSpecΓ_appTop, Scheme.ΓSpecIso_naturality, CommRingCat.comp_apply,
homOfVector_appTop_coord, Function.comp_apply, CommRingCat.coe_of, Scheme.id_app, CommRingCat.id_apply]
-- TODO: why does `simp` not apply this?
rw [CommRingCat.hom_inv_apply]
exact eval₂_X _ _ _
inv_hom_id := by
apply ext_of_isAffine
simp only [Scheme.comp_coeBase, TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top,
Scheme.comp_app, Scheme.toSpecΓ_appTop, Scheme.ΓSpecIso_naturality, Category.assoc, Scheme.id_app,
← Iso.eq_inv_comp, Category.comp_id]
ext : 1
apply ringHom_ext'
· change _ = (CommRingCat.ofHom C ≫ _).hom
rw [CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom, eval₂Hom_comp_C, ← CommRingCat.hom_comp, ←
CommRingCat.hom_ext_iff, ← cancel_mono (Scheme.ΓSpecIso _).hom]
rw [← Scheme.comp_appTop, homOfVector_over, Scheme.comp_appTop]
simp only [Category.assoc, Scheme.ΓSpecIso_naturality, CommRingCat.of_carrier, ← Scheme.toSpecΓ_appTop]
rw [← Scheme.comp_appTop_assoc, Scheme.isoSpec, asIso_inv, IsIso.hom_inv_id]
simp
· intro i
rw [CommRingCat.comp_apply, ConcreteCategory.hom_ofHom, coe_eval₂Hom]
simp only [eval₂_X]
exact homOfVector_appTop_coord _ _ _