English
The set of ring homomorphisms from the polynomial ring A[X_i] to R is homeomorphic to the product of Hom(A,R) with R^I, where I is the index set for X_i.
Русский
Множество кольцевых гомоморфизмов от кольца A[X_i] в R гомеоморфно произведению Hom(A,R) и R^I, где I — индекс множества X_i.
LaTeX
$$$\mathrm{Hom}(\mathrm{MvPolynomial}(\sigma, A), R) \simeq_t (\mathrm{Hom}(A,R) \times (\sigma \to R))$$$
Lean4
/-- `Hom(A[Xᵢ], R)` is homeomorphic to `Hom(A, R) × Rⁱ`. -/
@[simps! apply_fst apply_snd symm_apply_hom]
noncomputable def mvPolynomialHomeomorph (σ : Type v) (R A : CommRingCat.{max u v}) [TopologicalSpace R]
[IsTopologicalRing R] : (CommRingCat.of (MvPolynomial σ A) ⟶ R) ≃ₜ ((A ⟶ R) × (σ → R))
where
toFun f := ⟨CommRingCat.ofHom MvPolynomial.C ≫ f, fun i ↦ f (.X i)⟩
invFun fx := CommRingCat.ofHom (MvPolynomial.eval₂Hom fx.1.hom fx.2)
left_inv f := by ext <;> simp
right_inv fx := by ext <;> simp
continuous_toFun := by fun_prop
continuous_invFun := by
refine continuous_induced_rng.mpr ?_
refine continuous_pi fun p ↦ ?_
simp only [Function.comp_apply, hom_ofHom, MvPolynomial.coe_eval₂Hom, MvPolynomial.eval₂_eq]
fun_prop
