English
One component of the homEquiv construction asserts that evaluating the equivalent on indeterminates X_i recovers the original function on σ.
Русский
Компонент конструктора homEquiv утверждает, что при оценке через X_i восстанавливается исходная функция на σ.
LaTeX
$$$(\\mathrm{eval}_{2\\mathrm{Hom}}(\\mathrm{Int.castRingHom} S)\\; f) \\circ \\mathrm{X} = f$$$
Lean4
/-- Ring homomorphisms out of integer polynomials on a type `σ` are the same as
functions out of the type `σ`. -/
def homEquiv : (MvPolynomial σ ℤ →+* S) ≃ (σ → S)
where
toFun f := f ∘ X
invFun f := eval₂Hom (Int.castRingHom S) f
left_inv _ := RingHom.ext <| eval₂Hom_X _ _
right_inv f := funext fun x => by simp only [coe_eval₂Hom, Function.comp_apply, eval₂_X]
