of_mvPolynomial_int_ext — Mathlib

English

There is a canonical equivalence between morphisms X → Spec ℤ[n] and n-tuples of global sections of the structure sheaf on X.

Русский

Существует каноническое биективное соответствие между морфизмами X → Spec ℤ[n] и n-кортежами глобальных секций структуры на X.

LaTeX

$$$ X \to \mathrm{Spec}\, \mathbb{Z}[n] \quad \simeq \quad n \to \Gamma(X, \mathcal{O}_X) $$$

Lean4

theorem of_mvPolynomial_int_ext {R} {f g : ℤ[n] ⟶ R} (h : ∀ i, f (.X i) = g (.X i)) : f = g :=
  by
  suffices
    f.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom =
      g.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom
    by
    ext x
    · obtain ⟨x⟩ := x
      simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (C x)
    · simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (X x)
  ext1
  · exact RingHom.ext_int _ _
  · simpa using h _

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