isoOfIsAffine — Mathlib

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 _ _ _

Похожие утверждения