toSpecMvPolyIntEquiv — Mathlib

English

The above bijection is defined by sending a morphism to its coordinate evaluations and its inverse recovers a morphism from a tuple of global coordinates.

Русский

Указанная биекция задаётся отображением координатного набора morphisms и обратное за счёт полученного кортежа координат.

LaTeX

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

Lean4

/-- Morphisms into `Spec ℤ[n]` are equivalent the choice of `n` global sections.
Use `homOverEquiv` instead.
-/
@[simps]
def toSpecMvPolyIntEquiv : (X ⟶ Spec ℤ[n]) ≃ (n → Γ(X, ⊤))
    where
  toFun f i := f.appTop ((Scheme.ΓSpecIso ℤ[n]).inv (.X i))
  invFun
    v :=
    X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (MvPolynomial.eval₂Hom ((algebraMap ℤ _).comp ULift.ringEquiv.toRingHom) v))
  left_inv
    f := by
    apply (ΓSpec.adjunction.homEquiv _ _).symm.injective
    apply Quiver.Hom.unop_inj
    rw [Adjunction.homEquiv_symm_apply, Adjunction.homEquiv_symm_apply]
    simp only [Functor.rightOp_obj, Scheme.Γ_obj, Scheme.Spec_obj, algebraMap_int_eq, RingEquiv.toRingHom_eq_coe,
      TopologicalSpace.Opens.map_top, Functor.rightOp_map, op_comp, Scheme.Γ_map, unop_comp, Quiver.Hom.unop_op,
      Scheme.comp_app, Scheme.toSpecΓ_appTop, Scheme.ΓSpecIso_naturality, ΓSpec.adjunction_counit_app, Category.assoc,
      Iso.cancel_iso_inv_left, ← Iso.eq_inv_comp]
    apply of_mvPolynomial_int_ext
    intro i
    rw [ConcreteCategory.hom_ofHom, coe_eval₂Hom, eval₂_X]
    rfl
  right_inv
    v := by
    ext i
    simp only [algebraMap_int_eq, RingEquiv.toRingHom_eq_coe, TopologicalSpace.Opens.map_top, Scheme.comp_app,
      Scheme.toSpecΓ_appTop, Scheme.ΓSpecIso_naturality, CommRingCat.comp_apply, CommRingCat.coe_of]
      -- TODO: why does `simp` not apply this lemma?

    rw [CommRingCat.hom_inv_apply]
    simp

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